↳ ITRS
↳ ITRStoIDPProof
z
eval(x, y, z) → Cond_eval1(&&(>=@z(x, 0@z), >=@z(*@z(*@z(z, z), z), y)), x, y, z)
Cond_eval1(TRUE, x, y, z) → eval(x, -@z(y, 1@z), +@z(z, y))
Cond_eval(TRUE, x, y, z) → eval(-@z(x, 1@z), -@z(y, 1@z), z)
eval(x, y, z) → Cond_eval(&&(>=@z(x, 0@z), >=@z(*@z(*@z(z, z), z), y)), x, y, z)
eval(x0, x1, x2)
Cond_eval1(TRUE, x0, x1, x2)
Cond_eval(TRUE, x0, x1, x2)
↳ ITRS
↳ ITRStoIDPProof
↳ IDP
↳ UsableRulesProof
z
eval(x, y, z) → Cond_eval1(&&(>=@z(x, 0@z), >=@z(*@z(*@z(z, z), z), y)), x, y, z)
Cond_eval1(TRUE, x, y, z) → eval(x, -@z(y, 1@z), +@z(z, y))
Cond_eval(TRUE, x, y, z) → eval(-@z(x, 1@z), -@z(y, 1@z), z)
eval(x, y, z) → Cond_eval(&&(>=@z(x, 0@z), >=@z(*@z(*@z(z, z), z), y)), x, y, z)
(0) -> (1), if ((z[0] →* z[1])∧(x[0] →* x[1])∧(y[0] →* y[1])∧(&&(>=@z(x[0], 0@z), >=@z(*@z(*@z(z[0], z[0]), z[0]), y[0])) →* TRUE))
(1) -> (0), if ((-@z(y[1], 1@z) →* y[0])∧(+@z(z[1], y[1]) →* z[0])∧(x[1] →* x[0]))
(1) -> (2), if ((-@z(y[1], 1@z) →* y[2])∧(+@z(z[1], y[1]) →* z[2])∧(x[1] →* x[2]))
(2) -> (3), if ((z[2] →* z[3])∧(x[2] →* x[3])∧(y[2] →* y[3])∧(&&(>=@z(x[2], 0@z), >=@z(*@z(*@z(z[2], z[2]), z[2]), y[2])) →* TRUE))
(3) -> (0), if ((-@z(y[3], 1@z) →* y[0])∧(z[3] →* z[0])∧(-@z(x[3], 1@z) →* x[0]))
(3) -> (2), if ((-@z(y[3], 1@z) →* y[2])∧(z[3] →* z[2])∧(-@z(x[3], 1@z) →* x[2]))
eval(x0, x1, x2)
Cond_eval1(TRUE, x0, x1, x2)
Cond_eval(TRUE, x0, x1, x2)
↳ ITRS
↳ ITRStoIDPProof
↳ IDP
↳ UsableRulesProof
↳ IDP
↳ IDPNonInfProof
z
(0) -> (1), if ((z[0] →* z[1])∧(x[0] →* x[1])∧(y[0] →* y[1])∧(&&(>=@z(x[0], 0@z), >=@z(*@z(*@z(z[0], z[0]), z[0]), y[0])) →* TRUE))
(1) -> (0), if ((-@z(y[1], 1@z) →* y[0])∧(+@z(z[1], y[1]) →* z[0])∧(x[1] →* x[0]))
(1) -> (2), if ((-@z(y[1], 1@z) →* y[2])∧(+@z(z[1], y[1]) →* z[2])∧(x[1] →* x[2]))
(2) -> (3), if ((z[2] →* z[3])∧(x[2] →* x[3])∧(y[2] →* y[3])∧(&&(>=@z(x[2], 0@z), >=@z(*@z(*@z(z[2], z[2]), z[2]), y[2])) →* TRUE))
(3) -> (0), if ((-@z(y[3], 1@z) →* y[0])∧(z[3] →* z[0])∧(-@z(x[3], 1@z) →* x[0]))
(3) -> (2), if ((-@z(y[3], 1@z) →* y[2])∧(z[3] →* z[2])∧(-@z(x[3], 1@z) →* x[2]))
eval(x0, x1, x2)
Cond_eval1(TRUE, x0, x1, x2)
Cond_eval(TRUE, x0, x1, x2)
(1) (EVAL(x[0], y[0], z[0])≥NonInfC∧EVAL(x[0], y[0], z[0])≥COND_EVAL1(&&(>=@z(x[0], 0@z), >=@z(*@z(*@z(z[0], z[0]), z[0]), y[0])), x[0], y[0], z[0])∧(UIncreasing(COND_EVAL1(&&(>=@z(x[0], 0@z), >=@z(*@z(*@z(z[0], z[0]), z[0]), y[0])), x[0], y[0], z[0])), ≥))
(2) ((UIncreasing(COND_EVAL1(&&(>=@z(x[0], 0@z), >=@z(*@z(*@z(z[0], z[0]), z[0]), y[0])), x[0], y[0], z[0])), ≥)∧0 ≥ 0∧0 ≥ 0)
(3) ((UIncreasing(COND_EVAL1(&&(>=@z(x[0], 0@z), >=@z(*@z(*@z(z[0], z[0]), z[0]), y[0])), x[0], y[0], z[0])), ≥)∧0 ≥ 0∧0 ≥ 0)
(4) ((UIncreasing(COND_EVAL1(&&(>=@z(x[0], 0@z), >=@z(*@z(*@z(z[0], z[0]), z[0]), y[0])), x[0], y[0], z[0])), ≥)∧0 ≥ 0∧0 ≥ 0)
(5) (0 = 0∧0 = 0∧0 = 0∧(UIncreasing(COND_EVAL1(&&(>=@z(x[0], 0@z), >=@z(*@z(*@z(z[0], z[0]), z[0]), y[0])), x[0], y[0], z[0])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0)
(6) (+@z(z[1], y[1])=z[0]1∧x[1]=x[0]1∧y[0]=y[1]∧x[0]=x[1]∧z[0]=z[1]∧-@z(y[1], 1@z)=y[0]1∧&&(>=@z(x[0], 0@z), >=@z(*@z(*@z(z[0], z[0]), z[0]), y[0]))=TRUE ⇒ COND_EVAL1(TRUE, x[1], y[1], z[1])≥NonInfC∧COND_EVAL1(TRUE, x[1], y[1], z[1])≥EVAL(x[1], -@z(y[1], 1@z), +@z(z[1], y[1]))∧(UIncreasing(EVAL(x[1], -@z(y[1], 1@z), +@z(z[1], y[1]))), ≥))
(7) (>=@z(x[0], 0@z)=TRUE∧>=@z(*@z(*@z(z[0], z[0]), z[0]), y[0])=TRUE ⇒ COND_EVAL1(TRUE, x[0], y[0], z[0])≥NonInfC∧COND_EVAL1(TRUE, x[0], y[0], z[0])≥EVAL(x[0], -@z(y[0], 1@z), +@z(z[0], y[0]))∧(UIncreasing(EVAL(x[1], -@z(y[1], 1@z), +@z(z[1], y[1]))), ≥))
(8) (x[0] ≥ 0∧z[0]3 + (-1)y[0] ≥ 0 ⇒ (UIncreasing(EVAL(x[1], -@z(y[1], 1@z), +@z(z[1], y[1]))), ≥)∧0 ≥ 0∧0 ≥ 0)
(9) (x[0] ≥ 0∧z[0]3 + (-1)y[0] ≥ 0 ⇒ (UIncreasing(EVAL(x[1], -@z(y[1], 1@z), +@z(z[1], y[1]))), ≥)∧0 ≥ 0∧0 ≥ 0)
(10) (z[0]3 + (-1)y[0] ≥ 0∧x[0] ≥ 0 ⇒ 0 ≥ 0∧(UIncreasing(EVAL(x[1], -@z(y[1], 1@z), +@z(z[1], y[1]))), ≥)∧0 ≥ 0)
(11) (y[0] ≥ 0∧x[0] ≥ 0 ⇒ 0 ≥ 0∧(UIncreasing(EVAL(x[1], -@z(y[1], 1@z), +@z(z[1], y[1]))), ≥)∧0 ≥ 0)
(12) (y[0] ≥ 0∧x[0] ≥ 0∧z[0] ≥ 0 ⇒ 0 ≥ 0∧(UIncreasing(EVAL(x[1], -@z(y[1], 1@z), +@z(z[1], y[1]))), ≥)∧0 ≥ 0)
(13) (y[0] ≥ 0∧x[0] ≥ 0∧z[0] ≥ 0 ⇒ 0 ≥ 0∧(UIncreasing(EVAL(x[1], -@z(y[1], 1@z), +@z(z[1], y[1]))), ≥)∧0 ≥ 0)
(14) (x[1]=x[2]∧-@z(y[1], 1@z)=y[2]∧y[0]=y[1]∧+@z(z[1], y[1])=z[2]∧x[0]=x[1]∧z[0]=z[1]∧&&(>=@z(x[0], 0@z), >=@z(*@z(*@z(z[0], z[0]), z[0]), y[0]))=TRUE ⇒ COND_EVAL1(TRUE, x[1], y[1], z[1])≥NonInfC∧COND_EVAL1(TRUE, x[1], y[1], z[1])≥EVAL(x[1], -@z(y[1], 1@z), +@z(z[1], y[1]))∧(UIncreasing(EVAL(x[1], -@z(y[1], 1@z), +@z(z[1], y[1]))), ≥))
(15) (>=@z(x[0], 0@z)=TRUE∧>=@z(*@z(*@z(z[0], z[0]), z[0]), y[0])=TRUE ⇒ COND_EVAL1(TRUE, x[0], y[0], z[0])≥NonInfC∧COND_EVAL1(TRUE, x[0], y[0], z[0])≥EVAL(x[0], -@z(y[0], 1@z), +@z(z[0], y[0]))∧(UIncreasing(EVAL(x[1], -@z(y[1], 1@z), +@z(z[1], y[1]))), ≥))
(16) (x[0] ≥ 0∧z[0]3 + (-1)y[0] ≥ 0 ⇒ (UIncreasing(EVAL(x[1], -@z(y[1], 1@z), +@z(z[1], y[1]))), ≥)∧0 ≥ 0∧0 ≥ 0)
(17) (x[0] ≥ 0∧z[0]3 + (-1)y[0] ≥ 0 ⇒ (UIncreasing(EVAL(x[1], -@z(y[1], 1@z), +@z(z[1], y[1]))), ≥)∧0 ≥ 0∧0 ≥ 0)
(18) (x[0] ≥ 0∧z[0]3 + (-1)y[0] ≥ 0 ⇒ 0 ≥ 0∧(UIncreasing(EVAL(x[1], -@z(y[1], 1@z), +@z(z[1], y[1]))), ≥)∧0 ≥ 0)
(19) (x[0] ≥ 0∧y[0] ≥ 0 ⇒ 0 ≥ 0∧(UIncreasing(EVAL(x[1], -@z(y[1], 1@z), +@z(z[1], y[1]))), ≥)∧0 ≥ 0)
(20) (x[0] ≥ 0∧y[0] ≥ 0∧z[0] ≥ 0 ⇒ 0 ≥ 0∧(UIncreasing(EVAL(x[1], -@z(y[1], 1@z), +@z(z[1], y[1]))), ≥)∧0 ≥ 0)
(21) (x[0] ≥ 0∧y[0] ≥ 0∧z[0] ≥ 0 ⇒ 0 ≥ 0∧(UIncreasing(EVAL(x[1], -@z(y[1], 1@z), +@z(z[1], y[1]))), ≥)∧0 ≥ 0)
(22) (EVAL(x[2], y[2], z[2])≥NonInfC∧EVAL(x[2], y[2], z[2])≥COND_EVAL(&&(>=@z(x[2], 0@z), >=@z(*@z(*@z(z[2], z[2]), z[2]), y[2])), x[2], y[2], z[2])∧(UIncreasing(COND_EVAL(&&(>=@z(x[2], 0@z), >=@z(*@z(*@z(z[2], z[2]), z[2]), y[2])), x[2], y[2], z[2])), ≥))
(23) ((UIncreasing(COND_EVAL(&&(>=@z(x[2], 0@z), >=@z(*@z(*@z(z[2], z[2]), z[2]), y[2])), x[2], y[2], z[2])), ≥)∧0 ≥ 0∧0 ≥ 0)
(24) ((UIncreasing(COND_EVAL(&&(>=@z(x[2], 0@z), >=@z(*@z(*@z(z[2], z[2]), z[2]), y[2])), x[2], y[2], z[2])), ≥)∧0 ≥ 0∧0 ≥ 0)
(25) (0 ≥ 0∧0 ≥ 0∧(UIncreasing(COND_EVAL(&&(>=@z(x[2], 0@z), >=@z(*@z(*@z(z[2], z[2]), z[2]), y[2])), x[2], y[2], z[2])), ≥))
(26) (0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧(UIncreasing(COND_EVAL(&&(>=@z(x[2], 0@z), >=@z(*@z(*@z(z[2], z[2]), z[2]), y[2])), x[2], y[2], z[2])), ≥)∧0 ≥ 0∧0 = 0)
(27) (x[2]=x[3]∧y[2]=y[3]∧&&(>=@z(x[2], 0@z), >=@z(*@z(*@z(z[2], z[2]), z[2]), y[2]))=TRUE∧-@z(y[3], 1@z)=y[0]∧z[2]=z[3]∧-@z(x[3], 1@z)=x[0]∧z[3]=z[0] ⇒ COND_EVAL(TRUE, x[3], y[3], z[3])≥NonInfC∧COND_EVAL(TRUE, x[3], y[3], z[3])≥EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])∧(UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥))
(28) (>=@z(x[2], 0@z)=TRUE∧>=@z(*@z(*@z(z[2], z[2]), z[2]), y[2])=TRUE ⇒ COND_EVAL(TRUE, x[2], y[2], z[2])≥NonInfC∧COND_EVAL(TRUE, x[2], y[2], z[2])≥EVAL(-@z(x[2], 1@z), -@z(y[2], 1@z), z[2])∧(UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥))
(29) (x[2] ≥ 0∧z[2]3 + (-1)y[2] ≥ 0 ⇒ (UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥)∧-1 + (-1)Bound + x[2] ≥ 0∧0 ≥ 0)
(30) (x[2] ≥ 0∧z[2]3 + (-1)y[2] ≥ 0 ⇒ (UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥)∧-1 + (-1)Bound + x[2] ≥ 0∧0 ≥ 0)
(31) (x[2] ≥ 0∧z[2]3 + (-1)y[2] ≥ 0 ⇒ (UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥)∧0 ≥ 0∧-1 + (-1)Bound + x[2] ≥ 0)
(32) (x[2] ≥ 0∧y[2]3 + (3)y[2]2·z[2] + (3)y[2]·z[2]2 + z[2]3 + (-1)y[2] ≥ 0 ⇒ (UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥)∧0 ≥ 0∧-1 + (-1)Bound + x[2] ≥ 0)
(33) (x[2] ≥ 0∧y[2]3 + (3)y[2]2·z[2] + (3)y[2]·z[2]2 + z[2]3 + (-1)y[2] ≥ 0∧z[2] ≥ 0 ⇒ (UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥)∧0 ≥ 0∧-1 + (-1)Bound + x[2] ≥ 0)
(34) (x[2] ≥ 0∧y[2]3 + (-3)y[2]2·z[2] + (3)y[2]·z[2]2 + (-1)z[2]3 + (-1)y[2] ≥ 0∧z[2] ≥ 0 ⇒ (UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥)∧0 ≥ 0∧-1 + (-1)Bound + x[2] ≥ 0)
(35) (x[2] ≥ 0∧y[2]3 + (3)y[2]2·z[2] + (3)y[2]·z[2]2 + z[2]3 + (-1)y[2] ≥ 0∧z[2] ≥ 0∧y[2] ≥ 0 ⇒ (UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥)∧0 ≥ 0∧-1 + (-1)Bound + x[2] ≥ 0)
(36) (x[2] ≥ 0∧(-1)y[2]3 + (3)y[2]2·z[2] + (-3)y[2]·z[2]2 + z[2]3 + y[2] ≥ 0∧z[2] ≥ 0∧y[2] ≥ 0 ⇒ (UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥)∧0 ≥ 0∧-1 + (-1)Bound + x[2] ≥ 0)
(37) (x[2] ≥ 0∧(-1)y[2]3 + (-3)y[2]2·z[2] + (-3)y[2]·z[2]2 + (-1)z[2]3 + y[2] ≥ 0∧z[2] ≥ 0∧y[2] ≥ 0 ⇒ (UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥)∧0 ≥ 0∧-1 + (-1)Bound + x[2] ≥ 0)
(38) (x[2] ≥ 0∧y[2]3 + (-3)y[2]2·z[2] + (3)y[2]·z[2]2 + (-1)z[2]3 + (-1)y[2] ≥ 0∧z[2] ≥ 0∧y[2] ≥ 0 ⇒ (UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥)∧0 ≥ 0∧-1 + (-1)Bound + x[2] ≥ 0)
(39) (x[2]=x[3]∧y[2]=y[3]∧&&(>=@z(x[2], 0@z), >=@z(*@z(*@z(z[2], z[2]), z[2]), y[2]))=TRUE∧z[2]=z[3]∧z[3]=z[2]1∧-@z(x[3], 1@z)=x[2]1∧-@z(y[3], 1@z)=y[2]1 ⇒ COND_EVAL(TRUE, x[3], y[3], z[3])≥NonInfC∧COND_EVAL(TRUE, x[3], y[3], z[3])≥EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])∧(UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥))
(40) (>=@z(x[2], 0@z)=TRUE∧>=@z(*@z(*@z(z[2], z[2]), z[2]), y[2])=TRUE ⇒ COND_EVAL(TRUE, x[2], y[2], z[2])≥NonInfC∧COND_EVAL(TRUE, x[2], y[2], z[2])≥EVAL(-@z(x[2], 1@z), -@z(y[2], 1@z), z[2])∧(UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥))
(41) (x[2] ≥ 0∧z[2]3 + (-1)y[2] ≥ 0 ⇒ (UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥)∧-1 + (-1)Bound + x[2] ≥ 0∧0 ≥ 0)
(42) (x[2] ≥ 0∧z[2]3 + (-1)y[2] ≥ 0 ⇒ (UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥)∧-1 + (-1)Bound + x[2] ≥ 0∧0 ≥ 0)
(43) (x[2] ≥ 0∧z[2]3 + (-1)y[2] ≥ 0 ⇒ 0 ≥ 0∧(UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥)∧-1 + (-1)Bound + x[2] ≥ 0)
(44) (x[2] ≥ 0∧y[2]3 + (3)y[2]2·z[2] + (3)y[2]·z[2]2 + z[2]3 + (-1)y[2] ≥ 0 ⇒ 0 ≥ 0∧(UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥)∧-1 + (-1)Bound + x[2] ≥ 0)
(45) (x[2] ≥ 0∧y[2]3 + (3)y[2]2·z[2] + (3)y[2]·z[2]2 + z[2]3 + (-1)y[2] ≥ 0∧z[2] ≥ 0 ⇒ 0 ≥ 0∧(UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥)∧-1 + (-1)Bound + x[2] ≥ 0)
(46) (x[2] ≥ 0∧y[2]3 + (-3)y[2]2·z[2] + (3)y[2]·z[2]2 + (-1)z[2]3 + (-1)y[2] ≥ 0∧z[2] ≥ 0 ⇒ 0 ≥ 0∧(UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥)∧-1 + (-1)Bound + x[2] ≥ 0)
(47) (x[2] ≥ 0∧y[2]3 + (3)y[2]2·z[2] + (3)y[2]·z[2]2 + z[2]3 + (-1)y[2] ≥ 0∧z[2] ≥ 0∧y[2] ≥ 0 ⇒ 0 ≥ 0∧(UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥)∧-1 + (-1)Bound + x[2] ≥ 0)
(48) (x[2] ≥ 0∧(-1)y[2]3 + (3)y[2]2·z[2] + (-3)y[2]·z[2]2 + z[2]3 + y[2] ≥ 0∧z[2] ≥ 0∧y[2] ≥ 0 ⇒ 0 ≥ 0∧(UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥)∧-1 + (-1)Bound + x[2] ≥ 0)
(49) (x[2] ≥ 0∧(-1)y[2]3 + (-3)y[2]2·z[2] + (-3)y[2]·z[2]2 + (-1)z[2]3 + y[2] ≥ 0∧z[2] ≥ 0∧y[2] ≥ 0 ⇒ 0 ≥ 0∧(UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥)∧-1 + (-1)Bound + x[2] ≥ 0)
(50) (x[2] ≥ 0∧y[2]3 + (-3)y[2]2·z[2] + (3)y[2]·z[2]2 + (-1)z[2]3 + (-1)y[2] ≥ 0∧z[2] ≥ 0∧y[2] ≥ 0 ⇒ 0 ≥ 0∧(UIncreasing(EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])), ≥)∧-1 + (-1)Bound + x[2] ≥ 0)
POL(-@z(x1, x2)) = x1 + (-1)x2
POL(0@z) = 0
POL(*@z(x1, x2)) = x1·x2
POL(TRUE) = 0
POL(&&(x1, x2)) = 0
POL(EVAL(x1, x2, x3)) = -1 + x1
POL(FALSE) = 2
POL(>=@z(x1, x2)) = -1
POL(COND_EVAL1(x1, x2, x3, x4)) = -1 + x2 + (-1)x1
POL(+@z(x1, x2)) = x1 + x2
POL(COND_EVAL(x1, x2, x3, x4)) = -1 + x2 + (-1)x1
POL(1@z) = 1
POL(undefined) = -1
COND_EVAL(TRUE, x[3], y[3], z[3]) → EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])
COND_EVAL(TRUE, x[3], y[3], z[3]) → EVAL(-@z(x[3], 1@z), -@z(y[3], 1@z), z[3])
EVAL(x[0], y[0], z[0]) → COND_EVAL1(&&(>=@z(x[0], 0@z), >=@z(*@z(*@z(z[0], z[0]), z[0]), y[0])), x[0], y[0], z[0])
COND_EVAL1(TRUE, x[1], y[1], z[1]) → EVAL(x[1], -@z(y[1], 1@z), +@z(z[1], y[1]))
EVAL(x[2], y[2], z[2]) → COND_EVAL(&&(>=@z(x[2], 0@z), >=@z(*@z(*@z(z[2], z[2]), z[2]), y[2])), x[2], y[2], z[2])
FALSE1 → &&(FALSE, FALSE)1
-@z1 ↔
TRUE1 → &&(TRUE, TRUE)1
+@z1 ↔
FALSE1 → &&(TRUE, FALSE)1
FALSE1 → &&(FALSE, TRUE)1
↳ ITRS
↳ ITRStoIDPProof
↳ IDP
↳ UsableRulesProof
↳ IDP
↳ IDPNonInfProof
↳ IDP
↳ IDependencyGraphProof
z
(1) -> (2), if ((-@z(y[1], 1@z) →* y[2])∧(+@z(z[1], y[1]) →* z[2])∧(x[1] →* x[2]))
(0) -> (1), if ((z[0] →* z[1])∧(x[0] →* x[1])∧(y[0] →* y[1])∧(&&(>=@z(x[0], 0@z), >=@z(*@z(*@z(z[0], z[0]), z[0]), y[0])) →* TRUE))
(1) -> (0), if ((-@z(y[1], 1@z) →* y[0])∧(+@z(z[1], y[1]) →* z[0])∧(x[1] →* x[0]))
eval(x0, x1, x2)
Cond_eval1(TRUE, x0, x1, x2)
Cond_eval(TRUE, x0, x1, x2)
↳ ITRS
↳ ITRStoIDPProof
↳ IDP
↳ UsableRulesProof
↳ IDP
↳ IDPNonInfProof
↳ IDP
↳ IDependencyGraphProof
↳ IDP
↳ IDPtoQDPProof
z
(0) -> (1), if ((z[0] →* z[1])∧(x[0] →* x[1])∧(y[0] →* y[1])∧(&&(>=@z(x[0], 0@z), >=@z(*@z(*@z(z[0], z[0]), z[0]), y[0])) →* TRUE))
(1) -> (0), if ((-@z(y[1], 1@z) →* y[0])∧(+@z(z[1], y[1]) →* z[0])∧(x[1] →* x[0]))
eval(x0, x1, x2)
Cond_eval1(TRUE, x0, x1, x2)
Cond_eval(TRUE, x0, x1, x2)
↳ ITRS
↳ ITRStoIDPProof
↳ IDP
↳ UsableRulesProof
↳ IDP
↳ IDPNonInfProof
↳ IDP
↳ IDependencyGraphProof
↳ IDP
↳ IDPtoQDPProof
↳ QDP
↳ UsableRulesProof
COND_EVAL1(true, x[1], y[1], z[1]) → EVAL(x[1], minus_int(y[1], pos(s(0))), plus_int(z[1], y[1]))
EVAL(x[0], y[0], z[0]) → COND_EVAL1(and(greatereq_int(x[0], pos(0)), greatereq_int(mult_int(mult_int(z[0], z[0]), z[0]), y[0])), x[0], y[0], z[0])
minus_int(pos(x), pos(y)) → minus_nat(x, y)
minus_int(neg(x), neg(y)) → minus_nat(y, x)
minus_int(neg(x), pos(y)) → neg(plus_nat(x, y))
minus_int(pos(x), neg(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
eval(x0, x1, x2)
Cond_eval1(true, x0, x1, x2)
Cond_eval(true, x0, x1, x2)
minus_int(pos(x0), pos(x1))
minus_int(neg(x0), neg(x1))
minus_int(neg(x0), pos(x1))
minus_int(pos(x0), neg(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoIDPProof
↳ IDP
↳ UsableRulesProof
↳ IDP
↳ IDPNonInfProof
↳ IDP
↳ IDependencyGraphProof
↳ IDP
↳ IDPtoQDPProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
COND_EVAL1(true, x[1], y[1], z[1]) → EVAL(x[1], minus_int(y[1], pos(s(0))), plus_int(z[1], y[1]))
EVAL(x[0], y[0], z[0]) → COND_EVAL1(and(greatereq_int(x[0], pos(0)), greatereq_int(mult_int(mult_int(z[0], z[0]), z[0]), y[0])), x[0], y[0], z[0])
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_int(pos(x), pos(y)) → minus_nat(x, y)
minus_int(neg(x), pos(y)) → neg(plus_nat(x, y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
eval(x0, x1, x2)
Cond_eval1(true, x0, x1, x2)
Cond_eval(true, x0, x1, x2)
minus_int(pos(x0), pos(x1))
minus_int(neg(x0), neg(x1))
minus_int(neg(x0), pos(x1))
minus_int(pos(x0), neg(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
eval(x0, x1, x2)
Cond_eval1(true, x0, x1, x2)
Cond_eval(true, x0, x1, x2)
↳ ITRS
↳ ITRStoIDPProof
↳ IDP
↳ UsableRulesProof
↳ IDP
↳ IDPNonInfProof
↳ IDP
↳ IDependencyGraphProof
↳ IDP
↳ IDPtoQDPProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
COND_EVAL1(true, x[1], y[1], z[1]) → EVAL(x[1], minus_int(y[1], pos(s(0))), plus_int(z[1], y[1]))
EVAL(x[0], y[0], z[0]) → COND_EVAL1(and(greatereq_int(x[0], pos(0)), greatereq_int(mult_int(mult_int(z[0], z[0]), z[0]), y[0])), x[0], y[0], z[0])
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_int(pos(x), pos(y)) → minus_nat(x, y)
minus_int(neg(x), pos(y)) → neg(plus_nat(x, y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_int(pos(x0), pos(x1))
minus_int(neg(x0), neg(x1))
minus_int(neg(x0), pos(x1))
minus_int(pos(x0), neg(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoIDPProof
↳ IDP
↳ UsableRulesProof
↳ IDP
↳ IDPNonInfProof
↳ IDP
↳ IDependencyGraphProof
↳ IDP
↳ IDPtoQDPProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ QDP
↳ RemovalProof
↳ Narrowing
COND_EVAL1(true, x[1], y[1], z[1], x_removed) → EVAL(x[1], minus_int(y[1], x_removed), plus_int(z[1], y[1]), x_removed)
EVAL(x[0], y[0], z[0], x_removed) → COND_EVAL1(and(greatereq_int(x[0], pos(0)), greatereq_int(mult_int(mult_int(z[0], z[0]), z[0]), y[0])), x[0], y[0], z[0], x_removed)
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_int(pos(x), pos(y)) → minus_nat(x, y)
minus_int(neg(x), pos(y)) → neg(plus_nat(x, y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_int(pos(x0), pos(x1))
minus_int(neg(x0), neg(x1))
minus_int(neg(x0), pos(x1))
minus_int(pos(x0), neg(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoIDPProof
↳ IDP
↳ UsableRulesProof
↳ IDP
↳ IDPNonInfProof
↳ IDP
↳ IDependencyGraphProof
↳ IDP
↳ IDPtoQDPProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ QDP
↳ Narrowing
COND_EVAL1(true, x[1], y[1], z[1], x_removed) → EVAL(x[1], minus_int(y[1], x_removed), plus_int(z[1], y[1]), x_removed)
EVAL(x[0], y[0], z[0], x_removed) → COND_EVAL1(and(greatereq_int(x[0], pos(0)), greatereq_int(mult_int(mult_int(z[0], z[0]), z[0]), y[0])), x[0], y[0], z[0], x_removed)
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_int(pos(x), pos(y)) → minus_nat(x, y)
minus_int(neg(x), pos(y)) → neg(plus_nat(x, y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_int(pos(x0), pos(x1))
minus_int(neg(x0), neg(x1))
minus_int(neg(x0), pos(x1))
minus_int(pos(x0), neg(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
EVAL(y0, y1, neg(x0)) → COND_EVAL1(and(greatereq_int(y0, pos(0)), greatereq_int(mult_int(pos(mult_nat(x0, x0)), neg(x0)), y1)), y0, y1, neg(x0))
EVAL(y0, y1, pos(x0)) → COND_EVAL1(and(greatereq_int(y0, pos(0)), greatereq_int(mult_int(pos(mult_nat(x0, x0)), pos(x0)), y1)), y0, y1, pos(x0))
EVAL(neg(s(x0)), y1, y2) → COND_EVAL1(and(false, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), neg(s(x0)), y1, y2)
EVAL(neg(0), y1, y2) → COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), neg(0), y1, y2)
EVAL(pos(x0), y1, y2) → COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), pos(x0), y1, y2)
↳ ITRS
↳ ITRStoIDPProof
↳ IDP
↳ UsableRulesProof
↳ IDP
↳ IDPNonInfProof
↳ IDP
↳ IDependencyGraphProof
↳ IDP
↳ IDPtoQDPProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
COND_EVAL1(true, x[1], y[1], z[1]) → EVAL(x[1], minus_int(y[1], pos(s(0))), plus_int(z[1], y[1]))
EVAL(y0, y1, neg(x0)) → COND_EVAL1(and(greatereq_int(y0, pos(0)), greatereq_int(mult_int(pos(mult_nat(x0, x0)), neg(x0)), y1)), y0, y1, neg(x0))
EVAL(y0, y1, pos(x0)) → COND_EVAL1(and(greatereq_int(y0, pos(0)), greatereq_int(mult_int(pos(mult_nat(x0, x0)), pos(x0)), y1)), y0, y1, pos(x0))
EVAL(neg(s(x0)), y1, y2) → COND_EVAL1(and(false, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), neg(s(x0)), y1, y2)
EVAL(neg(0), y1, y2) → COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), neg(0), y1, y2)
EVAL(pos(x0), y1, y2) → COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), pos(x0), y1, y2)
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_int(pos(x), pos(y)) → minus_nat(x, y)
minus_int(neg(x), pos(y)) → neg(plus_nat(x, y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_int(pos(x0), pos(x1))
minus_int(neg(x0), neg(x1))
minus_int(neg(x0), pos(x1))
minus_int(pos(x0), neg(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
EVAL(y0, y1, neg(x0)) → COND_EVAL1(and(greatereq_int(y0, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x0, x0), x0)), y1)), y0, y1, neg(x0))
↳ ITRS
↳ ITRStoIDPProof
↳ IDP
↳ UsableRulesProof
↳ IDP
↳ IDPNonInfProof
↳ IDP
↳ IDependencyGraphProof
↳ IDP
↳ IDPtoQDPProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
COND_EVAL1(true, x[1], y[1], z[1]) → EVAL(x[1], minus_int(y[1], pos(s(0))), plus_int(z[1], y[1]))
EVAL(y0, y1, pos(x0)) → COND_EVAL1(and(greatereq_int(y0, pos(0)), greatereq_int(mult_int(pos(mult_nat(x0, x0)), pos(x0)), y1)), y0, y1, pos(x0))
EVAL(neg(s(x0)), y1, y2) → COND_EVAL1(and(false, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), neg(s(x0)), y1, y2)
EVAL(neg(0), y1, y2) → COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), neg(0), y1, y2)
EVAL(pos(x0), y1, y2) → COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), pos(x0), y1, y2)
EVAL(y0, y1, neg(x0)) → COND_EVAL1(and(greatereq_int(y0, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x0, x0), x0)), y1)), y0, y1, neg(x0))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_int(pos(x), pos(y)) → minus_nat(x, y)
minus_int(neg(x), pos(y)) → neg(plus_nat(x, y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_int(pos(x0), pos(x1))
minus_int(neg(x0), neg(x1))
minus_int(neg(x0), pos(x1))
minus_int(pos(x0), neg(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
EVAL(y0, y1, pos(x0)) → COND_EVAL1(and(greatereq_int(y0, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x0, x0), x0)), y1)), y0, y1, pos(x0))
↳ ITRS
↳ ITRStoIDPProof
↳ IDP
↳ UsableRulesProof
↳ IDP
↳ IDPNonInfProof
↳ IDP
↳ IDependencyGraphProof
↳ IDP
↳ IDPtoQDPProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
COND_EVAL1(true, x[1], y[1], z[1]) → EVAL(x[1], minus_int(y[1], pos(s(0))), plus_int(z[1], y[1]))
EVAL(neg(s(x0)), y1, y2) → COND_EVAL1(and(false, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), neg(s(x0)), y1, y2)
EVAL(neg(0), y1, y2) → COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), neg(0), y1, y2)
EVAL(pos(x0), y1, y2) → COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), pos(x0), y1, y2)
EVAL(y0, y1, neg(x0)) → COND_EVAL1(and(greatereq_int(y0, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x0, x0), x0)), y1)), y0, y1, neg(x0))
EVAL(y0, y1, pos(x0)) → COND_EVAL1(and(greatereq_int(y0, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x0, x0), x0)), y1)), y0, y1, pos(x0))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_int(pos(x), pos(y)) → minus_nat(x, y)
minus_int(neg(x), pos(y)) → neg(plus_nat(x, y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_int(pos(x0), pos(x1))
minus_int(neg(x0), neg(x1))
minus_int(neg(x0), pos(x1))
minus_int(pos(x0), neg(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
COND_EVAL1(true, z0, z1, pos(z2)) → EVAL(z0, minus_int(z1, pos(s(0))), plus_int(pos(z2), z1))
COND_EVAL1(true, z0, z1, neg(z2)) → EVAL(z0, minus_int(z1, pos(s(0))), plus_int(neg(z2), z1))
COND_EVAL1(true, neg(0), z0, z1) → EVAL(neg(0), minus_int(z0, pos(s(0))), plus_int(z1, z0))
COND_EVAL1(true, pos(z0), z1, z2) → EVAL(pos(z0), minus_int(z1, pos(s(0))), plus_int(z2, z1))
COND_EVAL1(true, neg(s(z0)), z1, z2) → EVAL(neg(s(z0)), minus_int(z1, pos(s(0))), plus_int(z2, z1))
↳ ITRS
↳ ITRStoIDPProof
↳ IDP
↳ UsableRulesProof
↳ IDP
↳ IDPNonInfProof
↳ IDP
↳ IDependencyGraphProof
↳ IDP
↳ IDPtoQDPProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ QDPOrderProof
EVAL(neg(s(x0)), y1, y2) → COND_EVAL1(and(false, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), neg(s(x0)), y1, y2)
EVAL(neg(0), y1, y2) → COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), neg(0), y1, y2)
EVAL(pos(x0), y1, y2) → COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), pos(x0), y1, y2)
EVAL(y0, y1, neg(x0)) → COND_EVAL1(and(greatereq_int(y0, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x0, x0), x0)), y1)), y0, y1, neg(x0))
EVAL(y0, y1, pos(x0)) → COND_EVAL1(and(greatereq_int(y0, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x0, x0), x0)), y1)), y0, y1, pos(x0))
COND_EVAL1(true, z0, z1, pos(z2)) → EVAL(z0, minus_int(z1, pos(s(0))), plus_int(pos(z2), z1))
COND_EVAL1(true, z0, z1, neg(z2)) → EVAL(z0, minus_int(z1, pos(s(0))), plus_int(neg(z2), z1))
COND_EVAL1(true, neg(0), z0, z1) → EVAL(neg(0), minus_int(z0, pos(s(0))), plus_int(z1, z0))
COND_EVAL1(true, pos(z0), z1, z2) → EVAL(pos(z0), minus_int(z1, pos(s(0))), plus_int(z2, z1))
COND_EVAL1(true, neg(s(z0)), z1, z2) → EVAL(neg(s(z0)), minus_int(z1, pos(s(0))), plus_int(z2, z1))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_int(pos(x), pos(y)) → minus_nat(x, y)
minus_int(neg(x), pos(y)) → neg(plus_nat(x, y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_int(pos(x0), pos(x1))
minus_int(neg(x0), neg(x1))
minus_int(neg(x0), pos(x1))
minus_int(pos(x0), neg(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
EVAL(neg(s(x0)), y1, y2) → COND_EVAL1(and(false, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), neg(s(x0)), y1, y2)
Used ordering: Polynomial interpretation [POLO]:
EVAL(neg(0), y1, y2) → COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), neg(0), y1, y2)
EVAL(pos(x0), y1, y2) → COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), pos(x0), y1, y2)
EVAL(y0, y1, neg(x0)) → COND_EVAL1(and(greatereq_int(y0, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x0, x0), x0)), y1)), y0, y1, neg(x0))
EVAL(y0, y1, pos(x0)) → COND_EVAL1(and(greatereq_int(y0, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x0, x0), x0)), y1)), y0, y1, pos(x0))
COND_EVAL1(true, z0, z1, pos(z2)) → EVAL(z0, minus_int(z1, pos(s(0))), plus_int(pos(z2), z1))
COND_EVAL1(true, z0, z1, neg(z2)) → EVAL(z0, minus_int(z1, pos(s(0))), plus_int(neg(z2), z1))
COND_EVAL1(true, neg(0), z0, z1) → EVAL(neg(0), minus_int(z0, pos(s(0))), plus_int(z1, z0))
COND_EVAL1(true, pos(z0), z1, z2) → EVAL(pos(z0), minus_int(z1, pos(s(0))), plus_int(z2, z1))
COND_EVAL1(true, neg(s(z0)), z1, z2) → EVAL(neg(s(z0)), minus_int(z1, pos(s(0))), plus_int(z2, z1))
POL(0) = 0
POL(COND_EVAL1(x1, x2, x3, x4)) = x1
POL(EVAL(x1, x2, x3)) = 1
POL(and(x1, x2)) = x1
POL(false) = 0
POL(greatereq_int(x1, x2)) = x2
POL(minus_int(x1, x2)) = 0
POL(minus_nat(x1, x2)) = 0
POL(mult_int(x1, x2)) = 0
POL(mult_nat(x1, x2)) = 0
POL(neg(x1)) = 0
POL(plus_int(x1, x2)) = 0
POL(plus_nat(x1, x2)) = 0
POL(pos(x1)) = 1
POL(s(x1)) = 0
POL(true) = 1
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
and(true, true) → true
and(true, false) → false
and(false, true) → false
and(false, false) → false
↳ ITRS
↳ ITRStoIDPProof
↳ IDP
↳ UsableRulesProof
↳ IDP
↳ IDPNonInfProof
↳ IDP
↳ IDependencyGraphProof
↳ IDP
↳ IDPtoQDPProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ RemovalProof
EVAL(neg(0), y1, y2) → COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), neg(0), y1, y2)
EVAL(pos(x0), y1, y2) → COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), pos(x0), y1, y2)
EVAL(y0, y1, neg(x0)) → COND_EVAL1(and(greatereq_int(y0, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x0, x0), x0)), y1)), y0, y1, neg(x0))
EVAL(y0, y1, pos(x0)) → COND_EVAL1(and(greatereq_int(y0, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x0, x0), x0)), y1)), y0, y1, pos(x0))
COND_EVAL1(true, z0, z1, pos(z2)) → EVAL(z0, minus_int(z1, pos(s(0))), plus_int(pos(z2), z1))
COND_EVAL1(true, z0, z1, neg(z2)) → EVAL(z0, minus_int(z1, pos(s(0))), plus_int(neg(z2), z1))
COND_EVAL1(true, neg(0), z0, z1) → EVAL(neg(0), minus_int(z0, pos(s(0))), plus_int(z1, z0))
COND_EVAL1(true, pos(z0), z1, z2) → EVAL(pos(z0), minus_int(z1, pos(s(0))), plus_int(z2, z1))
COND_EVAL1(true, neg(s(z0)), z1, z2) → EVAL(neg(s(z0)), minus_int(z1, pos(s(0))), plus_int(z2, z1))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_int(pos(x), pos(y)) → minus_nat(x, y)
minus_int(neg(x), pos(y)) → neg(plus_nat(x, y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_int(pos(x0), pos(x1))
minus_int(neg(x0), neg(x1))
minus_int(neg(x0), pos(x1))
minus_int(pos(x0), neg(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoIDPProof
↳ IDP
↳ UsableRulesProof
↳ IDP
↳ IDPNonInfProof
↳ IDP
↳ IDependencyGraphProof
↳ IDP
↳ IDPtoQDPProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ RemovalProof
↳ QDP
↳ NonInfProof
EVAL(neg(0), y1, y2, x_removed) → COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), neg(0), y1, y2, x_removed)
COND_EVAL1(true, z0, z1, pos(z2), x_removed) → EVAL(z0, minus_int(z1, x_removed), plus_int(pos(z2), z1), x_removed)
COND_EVAL1(true, z0, z1, neg(z2), x_removed) → EVAL(z0, minus_int(z1, x_removed), plus_int(neg(z2), z1), x_removed)
COND_EVAL1(true, neg(0), z0, z1, x_removed) → EVAL(neg(0), minus_int(z0, x_removed), plus_int(z1, z0), x_removed)
EVAL(pos(x0), y1, y2, x_removed) → COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), pos(x0), y1, y2, x_removed)
COND_EVAL1(true, pos(z0), z1, z2, x_removed) → EVAL(pos(z0), minus_int(z1, x_removed), plus_int(z2, z1), x_removed)
EVAL(y0, y1, neg(x0), x_removed) → COND_EVAL1(and(greatereq_int(y0, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x0, x0), x0)), y1)), y0, y1, neg(x0), x_removed)
COND_EVAL1(true, neg(s(z0)), z1, z2, x_removed) → EVAL(neg(s(z0)), minus_int(z1, x_removed), plus_int(z2, z1), x_removed)
EVAL(y0, y1, pos(x0), x_removed) → COND_EVAL1(and(greatereq_int(y0, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x0, x0), x0)), y1)), y0, y1, pos(x0), x_removed)
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_int(pos(x), pos(y)) → minus_nat(x, y)
minus_int(neg(x), pos(y)) → neg(plus_nat(x, y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_int(pos(x0), pos(x1))
minus_int(neg(x0), neg(x1))
minus_int(neg(x0), pos(x1))
minus_int(pos(x0), neg(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
(1) (EVAL(x3, minus_int(x4, x6), plus_int(pos(x5), x4), x6)=EVAL(neg(0), x7, x8, x9) ⇒ EVAL(neg(0), x7, x8, x9)≥COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(x8, x8), x8), x7)), neg(0), x7, x8, x9))
(2) (EVAL(neg(0), x7, x8, x6)≥COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(x8, x8), x8), x7)), neg(0), x7, x8, x6))
(3) (EVAL(x10, minus_int(x11, x13), plus_int(neg(x12), x11), x13)=EVAL(neg(0), x14, x15, x16) ⇒ EVAL(neg(0), x14, x15, x16)≥COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(x15, x15), x15), x14)), neg(0), x14, x15, x16))
(4) (EVAL(neg(0), x14, x15, x13)≥COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(x15, x15), x15), x14)), neg(0), x14, x15, x13))
(5) (EVAL(neg(0), minus_int(x17, x19), plus_int(x18, x17), x19)=EVAL(neg(0), x20, x21, x22) ⇒ EVAL(neg(0), x20, x21, x22)≥COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(x21, x21), x21), x20)), neg(0), x20, x21, x22))
(6) (EVAL(neg(0), x20, x21, x19)≥COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(x21, x21), x21), x20)), neg(0), x20, x21, x19))
(7) (COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(x44, x44), x44), x43)), neg(0), x43, x44, x45)=COND_EVAL1(true, x46, x47, pos(x48), x49) ⇒ COND_EVAL1(true, x46, x47, pos(x48), x49)≥EVAL(x46, minus_int(x47, x49), plus_int(pos(x48), x47), x49))
(8) (true=x422∧greatereq_int(x424, x43)=x423∧and(x422, x423)=true ⇒ COND_EVAL1(true, neg(0), x43, pos(x48), x45)≥EVAL(neg(0), minus_int(x43, x45), plus_int(pos(x48), x43), x45))
(9) (true=true∧greatereq_int(x424, x43)=true ⇒ COND_EVAL1(true, neg(0), x43, pos(x48), x45)≥EVAL(neg(0), minus_int(x43, x45), plus_int(pos(x48), x43), x45))
(10) (greatereq_int(x424, x43)=true ⇒ COND_EVAL1(true, neg(0), x43, pos(x48), x45)≥EVAL(neg(0), minus_int(x43, x45), plus_int(pos(x48), x43), x45))
(11) (true=true ⇒ COND_EVAL1(true, neg(0), pos(0), pos(x48), x45)≥EVAL(neg(0), minus_int(pos(0), x45), plus_int(pos(x48), pos(0)), x45))
(12) (true=true ⇒ COND_EVAL1(true, neg(0), pos(0), pos(x48), x45)≥EVAL(neg(0), minus_int(pos(0), x45), plus_int(pos(x48), pos(0)), x45))
(13) (true=true ⇒ COND_EVAL1(true, neg(0), neg(x431), pos(x48), x45)≥EVAL(neg(0), minus_int(neg(x431), x45), plus_int(pos(x48), neg(x431)), x45))
(14) (true=true ⇒ COND_EVAL1(true, neg(0), neg(x432), pos(x48), x45)≥EVAL(neg(0), minus_int(neg(x432), x45), plus_int(pos(x48), neg(x432)), x45))
(15) (greatereq_int(pos(x439), pos(x438))=true∧(∀x440,x441:greatereq_int(pos(x439), pos(x438))=true ⇒ COND_EVAL1(true, neg(0), pos(x438), pos(x440), x441)≥EVAL(neg(0), minus_int(pos(x438), x441), plus_int(pos(x440), pos(x438)), x441)) ⇒ COND_EVAL1(true, neg(0), pos(s(x438)), pos(x48), x45)≥EVAL(neg(0), minus_int(pos(s(x438)), x45), plus_int(pos(x48), pos(s(x438))), x45))
(16) (greatereq_int(neg(x443), neg(x442))=true∧(∀x444,x445:greatereq_int(neg(x443), neg(x442))=true ⇒ COND_EVAL1(true, neg(0), neg(x442), pos(x444), x445)≥EVAL(neg(0), minus_int(neg(x442), x445), plus_int(pos(x444), neg(x442)), x445)) ⇒ COND_EVAL1(true, neg(0), neg(s(x442)), pos(x48), x45)≥EVAL(neg(0), minus_int(neg(s(x442)), x45), plus_int(pos(x48), neg(s(x442))), x45))
(17) (COND_EVAL1(true, neg(0), pos(0), pos(x48), x45)≥EVAL(neg(0), minus_int(pos(0), x45), plus_int(pos(x48), pos(0)), x45))
(18) (COND_EVAL1(true, neg(0), pos(0), pos(x48), x45)≥EVAL(neg(0), minus_int(pos(0), x45), plus_int(pos(x48), pos(0)), x45))
(19) (COND_EVAL1(true, neg(0), neg(x431), pos(x48), x45)≥EVAL(neg(0), minus_int(neg(x431), x45), plus_int(pos(x48), neg(x431)), x45))
(20) (COND_EVAL1(true, neg(0), neg(x432), pos(x48), x45)≥EVAL(neg(0), minus_int(neg(x432), x45), plus_int(pos(x48), neg(x432)), x45))
(21) (COND_EVAL1(true, neg(0), pos(x438), pos(x48), x45)≥EVAL(neg(0), minus_int(pos(x438), x45), plus_int(pos(x48), pos(x438)), x45) ⇒ COND_EVAL1(true, neg(0), pos(s(x438)), pos(x48), x45)≥EVAL(neg(0), minus_int(pos(s(x438)), x45), plus_int(pos(x48), pos(s(x438))), x45))
(22) (COND_EVAL1(true, neg(0), neg(x442), pos(x48), x45)≥EVAL(neg(0), minus_int(neg(x442), x45), plus_int(pos(x48), neg(x442)), x45) ⇒ COND_EVAL1(true, neg(0), neg(s(x442)), pos(x48), x45)≥EVAL(neg(0), minus_int(neg(s(x442)), x45), plus_int(pos(x48), neg(s(x442))), x45))
(23) (COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(x63, x63), x63), x62)), pos(x61), x62, x63, x64)=COND_EVAL1(true, x65, x66, pos(x67), x68) ⇒ COND_EVAL1(true, x65, x66, pos(x67), x68)≥EVAL(x65, minus_int(x66, x68), plus_int(pos(x67), x66), x68))
(24) (true=x446∧greatereq_int(x448, x62)=x447∧and(x446, x447)=true ⇒ COND_EVAL1(true, pos(x61), x62, pos(x67), x64)≥EVAL(pos(x61), minus_int(x62, x64), plus_int(pos(x67), x62), x64))
(25) (true=true∧greatereq_int(x448, x62)=true ⇒ COND_EVAL1(true, pos(x61), x62, pos(x67), x64)≥EVAL(pos(x61), minus_int(x62, x64), plus_int(pos(x67), x62), x64))
(26) (greatereq_int(x448, x62)=true ⇒ COND_EVAL1(true, pos(x61), x62, pos(x67), x64)≥EVAL(pos(x61), minus_int(x62, x64), plus_int(pos(x67), x62), x64))
(27) (true=true ⇒ COND_EVAL1(true, pos(x61), pos(0), pos(x67), x64)≥EVAL(pos(x61), minus_int(pos(0), x64), plus_int(pos(x67), pos(0)), x64))
(28) (true=true ⇒ COND_EVAL1(true, pos(x61), pos(0), pos(x67), x64)≥EVAL(pos(x61), minus_int(pos(0), x64), plus_int(pos(x67), pos(0)), x64))
(29) (true=true ⇒ COND_EVAL1(true, pos(x61), neg(x455), pos(x67), x64)≥EVAL(pos(x61), minus_int(neg(x455), x64), plus_int(pos(x67), neg(x455)), x64))
(30) (true=true ⇒ COND_EVAL1(true, pos(x61), neg(x456), pos(x67), x64)≥EVAL(pos(x61), minus_int(neg(x456), x64), plus_int(pos(x67), neg(x456)), x64))
(31) (greatereq_int(pos(x463), pos(x462))=true∧(∀x464,x465,x466:greatereq_int(pos(x463), pos(x462))=true ⇒ COND_EVAL1(true, pos(x464), pos(x462), pos(x465), x466)≥EVAL(pos(x464), minus_int(pos(x462), x466), plus_int(pos(x465), pos(x462)), x466)) ⇒ COND_EVAL1(true, pos(x61), pos(s(x462)), pos(x67), x64)≥EVAL(pos(x61), minus_int(pos(s(x462)), x64), plus_int(pos(x67), pos(s(x462))), x64))
(32) (greatereq_int(neg(x468), neg(x467))=true∧(∀x469,x470,x471:greatereq_int(neg(x468), neg(x467))=true ⇒ COND_EVAL1(true, pos(x469), neg(x467), pos(x470), x471)≥EVAL(pos(x469), minus_int(neg(x467), x471), plus_int(pos(x470), neg(x467)), x471)) ⇒ COND_EVAL1(true, pos(x61), neg(s(x467)), pos(x67), x64)≥EVAL(pos(x61), minus_int(neg(s(x467)), x64), plus_int(pos(x67), neg(s(x467))), x64))
(33) (COND_EVAL1(true, pos(x61), pos(0), pos(x67), x64)≥EVAL(pos(x61), minus_int(pos(0), x64), plus_int(pos(x67), pos(0)), x64))
(34) (COND_EVAL1(true, pos(x61), pos(0), pos(x67), x64)≥EVAL(pos(x61), minus_int(pos(0), x64), plus_int(pos(x67), pos(0)), x64))
(35) (COND_EVAL1(true, pos(x61), neg(x455), pos(x67), x64)≥EVAL(pos(x61), minus_int(neg(x455), x64), plus_int(pos(x67), neg(x455)), x64))
(36) (COND_EVAL1(true, pos(x61), neg(x456), pos(x67), x64)≥EVAL(pos(x61), minus_int(neg(x456), x64), plus_int(pos(x67), neg(x456)), x64))
(37) (COND_EVAL1(true, pos(x61), pos(x462), pos(x67), x64)≥EVAL(pos(x61), minus_int(pos(x462), x64), plus_int(pos(x67), pos(x462)), x64) ⇒ COND_EVAL1(true, pos(x61), pos(s(x462)), pos(x67), x64)≥EVAL(pos(x61), minus_int(pos(s(x462)), x64), plus_int(pos(x67), pos(s(x462))), x64))
(38) (COND_EVAL1(true, pos(x61), neg(x467), pos(x67), x64)≥EVAL(pos(x61), minus_int(neg(x467), x64), plus_int(pos(x67), neg(x467)), x64) ⇒ COND_EVAL1(true, pos(x61), neg(s(x467)), pos(x67), x64)≥EVAL(pos(x61), minus_int(neg(s(x467)), x64), plus_int(pos(x67), neg(s(x467))), x64))
(39) (COND_EVAL1(and(greatereq_int(x81, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x83, x83), x83)), x82)), x81, x82, pos(x83), x84)=COND_EVAL1(true, x85, x86, pos(x87), x88) ⇒ COND_EVAL1(true, x85, x86, pos(x87), x88)≥EVAL(x85, minus_int(x86, x88), plus_int(pos(x87), x86), x88))
(40) (pos(0)=x474∧greatereq_int(x81, x474)=x472∧greatereq_int(x475, x82)=x473∧and(x472, x473)=true ⇒ COND_EVAL1(true, x81, x82, pos(x83), x84)≥EVAL(x81, minus_int(x82, x84), plus_int(pos(x83), x82), x84))
(41) (true=true∧pos(0)=x474∧greatereq_int(x81, x474)=true∧greatereq_int(x475, x82)=true ⇒ COND_EVAL1(true, x81, x82, pos(x83), x84)≥EVAL(x81, minus_int(x82, x84), plus_int(pos(x83), x82), x84))
(42) (pos(0)=x474∧greatereq_int(x81, x474)=true∧greatereq_int(x475, x82)=true ⇒ COND_EVAL1(true, x81, x82, pos(x83), x84)≥EVAL(x81, minus_int(x82, x84), plus_int(pos(x83), x82), x84))
(43) (true=true∧pos(0)=pos(0)∧greatereq_int(x475, x82)=true ⇒ COND_EVAL1(true, pos(x476), x82, pos(x83), x84)≥EVAL(pos(x476), minus_int(x82, x84), plus_int(pos(x83), x82), x84))
(44) (true=true∧pos(0)=pos(0)∧greatereq_int(x475, x82)=true ⇒ COND_EVAL1(true, neg(0), x82, pos(x83), x84)≥EVAL(neg(0), minus_int(x82, x84), plus_int(pos(x83), x82), x84))
(45) (true=true∧pos(0)=neg(x478)∧greatereq_int(x475, x82)=true ⇒ COND_EVAL1(true, neg(0), x82, pos(x83), x84)≥EVAL(neg(0), minus_int(x82, x84), plus_int(pos(x83), x82), x84))
(46) (true=true∧pos(0)=neg(x479)∧greatereq_int(x475, x82)=true ⇒ COND_EVAL1(true, pos(x480), x82, pos(x83), x84)≥EVAL(pos(x480), minus_int(x82, x84), plus_int(pos(x83), x82), x84))
(47) (greatereq_int(pos(x486), pos(x485))=true∧pos(0)=pos(s(x485))∧greatereq_int(x475, x82)=true∧(∀x487,x488,x489,x490:greatereq_int(pos(x486), pos(x485))=true∧pos(0)=pos(x485)∧greatereq_int(x487, x488)=true ⇒ COND_EVAL1(true, pos(x486), x488, pos(x489), x490)≥EVAL(pos(x486), minus_int(x488, x490), plus_int(pos(x489), x488), x490)) ⇒ COND_EVAL1(true, pos(s(x486)), x82, pos(x83), x84)≥EVAL(pos(s(x486)), minus_int(x82, x84), plus_int(pos(x83), x82), x84))
(48) (greatereq_int(neg(x492), neg(x491))=true∧pos(0)=neg(s(x491))∧greatereq_int(x475, x82)=true∧(∀x493,x494,x495,x496:greatereq_int(neg(x492), neg(x491))=true∧pos(0)=neg(x491)∧greatereq_int(x493, x494)=true ⇒ COND_EVAL1(true, neg(x492), x494, pos(x495), x496)≥EVAL(neg(x492), minus_int(x494, x496), plus_int(pos(x495), x494), x496)) ⇒ COND_EVAL1(true, neg(s(x492)), x82, pos(x83), x84)≥EVAL(neg(s(x492)), minus_int(x82, x84), plus_int(pos(x83), x82), x84))
(49) (greatereq_int(x475, x82)=true ⇒ COND_EVAL1(true, pos(x476), x82, pos(x83), x84)≥EVAL(pos(x476), minus_int(x82, x84), plus_int(pos(x83), x82), x84))
(50) (greatereq_int(x475, x82)=true ⇒ COND_EVAL1(true, neg(0), x82, pos(x83), x84)≥EVAL(neg(0), minus_int(x82, x84), plus_int(pos(x83), x82), x84))
(51) (true=true ⇒ COND_EVAL1(true, pos(x476), pos(0), pos(x83), x84)≥EVAL(pos(x476), minus_int(pos(0), x84), plus_int(pos(x83), pos(0)), x84))
(52) (true=true ⇒ COND_EVAL1(true, pos(x476), pos(0), pos(x83), x84)≥EVAL(pos(x476), minus_int(pos(0), x84), plus_int(pos(x83), pos(0)), x84))
(53) (true=true ⇒ COND_EVAL1(true, pos(x476), neg(x499), pos(x83), x84)≥EVAL(pos(x476), minus_int(neg(x499), x84), plus_int(pos(x83), neg(x499)), x84))
(54) (true=true ⇒ COND_EVAL1(true, pos(x476), neg(x500), pos(x83), x84)≥EVAL(pos(x476), minus_int(neg(x500), x84), plus_int(pos(x83), neg(x500)), x84))
(55) (greatereq_int(pos(x507), pos(x506))=true∧(∀x508,x509,x510:greatereq_int(pos(x507), pos(x506))=true ⇒ COND_EVAL1(true, pos(x508), pos(x506), pos(x509), x510)≥EVAL(pos(x508), minus_int(pos(x506), x510), plus_int(pos(x509), pos(x506)), x510)) ⇒ COND_EVAL1(true, pos(x476), pos(s(x506)), pos(x83), x84)≥EVAL(pos(x476), minus_int(pos(s(x506)), x84), plus_int(pos(x83), pos(s(x506))), x84))
(56) (greatereq_int(neg(x512), neg(x511))=true∧(∀x513,x514,x515:greatereq_int(neg(x512), neg(x511))=true ⇒ COND_EVAL1(true, pos(x513), neg(x511), pos(x514), x515)≥EVAL(pos(x513), minus_int(neg(x511), x515), plus_int(pos(x514), neg(x511)), x515)) ⇒ COND_EVAL1(true, pos(x476), neg(s(x511)), pos(x83), x84)≥EVAL(pos(x476), minus_int(neg(s(x511)), x84), plus_int(pos(x83), neg(s(x511))), x84))
(57) (COND_EVAL1(true, pos(x476), pos(0), pos(x83), x84)≥EVAL(pos(x476), minus_int(pos(0), x84), plus_int(pos(x83), pos(0)), x84))
(58) (COND_EVAL1(true, pos(x476), pos(0), pos(x83), x84)≥EVAL(pos(x476), minus_int(pos(0), x84), plus_int(pos(x83), pos(0)), x84))
(59) (COND_EVAL1(true, pos(x476), neg(x499), pos(x83), x84)≥EVAL(pos(x476), minus_int(neg(x499), x84), plus_int(pos(x83), neg(x499)), x84))
(60) (COND_EVAL1(true, pos(x476), neg(x500), pos(x83), x84)≥EVAL(pos(x476), minus_int(neg(x500), x84), plus_int(pos(x83), neg(x500)), x84))
(61) (COND_EVAL1(true, pos(x476), pos(x506), pos(x83), x84)≥EVAL(pos(x476), minus_int(pos(x506), x84), plus_int(pos(x83), pos(x506)), x84) ⇒ COND_EVAL1(true, pos(x476), pos(s(x506)), pos(x83), x84)≥EVAL(pos(x476), minus_int(pos(s(x506)), x84), plus_int(pos(x83), pos(s(x506))), x84))
(62) (COND_EVAL1(true, pos(x476), neg(x511), pos(x83), x84)≥EVAL(pos(x476), minus_int(neg(x511), x84), plus_int(pos(x83), neg(x511)), x84) ⇒ COND_EVAL1(true, pos(x476), neg(s(x511)), pos(x83), x84)≥EVAL(pos(x476), minus_int(neg(s(x511)), x84), plus_int(pos(x83), neg(s(x511))), x84))
(63) (true=true ⇒ COND_EVAL1(true, neg(0), pos(0), pos(x83), x84)≥EVAL(neg(0), minus_int(pos(0), x84), plus_int(pos(x83), pos(0)), x84))
(64) (true=true ⇒ COND_EVAL1(true, neg(0), pos(0), pos(x83), x84)≥EVAL(neg(0), minus_int(pos(0), x84), plus_int(pos(x83), pos(0)), x84))
(65) (true=true ⇒ COND_EVAL1(true, neg(0), neg(x518), pos(x83), x84)≥EVAL(neg(0), minus_int(neg(x518), x84), plus_int(pos(x83), neg(x518)), x84))
(66) (true=true ⇒ COND_EVAL1(true, neg(0), neg(x519), pos(x83), x84)≥EVAL(neg(0), minus_int(neg(x519), x84), plus_int(pos(x83), neg(x519)), x84))
(67) (greatereq_int(pos(x526), pos(x525))=true∧(∀x527,x528:greatereq_int(pos(x526), pos(x525))=true ⇒ COND_EVAL1(true, neg(0), pos(x525), pos(x527), x528)≥EVAL(neg(0), minus_int(pos(x525), x528), plus_int(pos(x527), pos(x525)), x528)) ⇒ COND_EVAL1(true, neg(0), pos(s(x525)), pos(x83), x84)≥EVAL(neg(0), minus_int(pos(s(x525)), x84), plus_int(pos(x83), pos(s(x525))), x84))
(68) (greatereq_int(neg(x530), neg(x529))=true∧(∀x531,x532:greatereq_int(neg(x530), neg(x529))=true ⇒ COND_EVAL1(true, neg(0), neg(x529), pos(x531), x532)≥EVAL(neg(0), minus_int(neg(x529), x532), plus_int(pos(x531), neg(x529)), x532)) ⇒ COND_EVAL1(true, neg(0), neg(s(x529)), pos(x83), x84)≥EVAL(neg(0), minus_int(neg(s(x529)), x84), plus_int(pos(x83), neg(s(x529))), x84))
(69) (COND_EVAL1(true, neg(0), pos(0), pos(x83), x84)≥EVAL(neg(0), minus_int(pos(0), x84), plus_int(pos(x83), pos(0)), x84))
(70) (COND_EVAL1(true, neg(0), pos(0), pos(x83), x84)≥EVAL(neg(0), minus_int(pos(0), x84), plus_int(pos(x83), pos(0)), x84))
(71) (COND_EVAL1(true, neg(0), neg(x518), pos(x83), x84)≥EVAL(neg(0), minus_int(neg(x518), x84), plus_int(pos(x83), neg(x518)), x84))
(72) (COND_EVAL1(true, neg(0), neg(x519), pos(x83), x84)≥EVAL(neg(0), minus_int(neg(x519), x84), plus_int(pos(x83), neg(x519)), x84))
(73) (COND_EVAL1(true, neg(0), pos(x525), pos(x83), x84)≥EVAL(neg(0), minus_int(pos(x525), x84), plus_int(pos(x83), pos(x525)), x84) ⇒ COND_EVAL1(true, neg(0), pos(s(x525)), pos(x83), x84)≥EVAL(neg(0), minus_int(pos(s(x525)), x84), plus_int(pos(x83), pos(s(x525))), x84))
(74) (COND_EVAL1(true, neg(0), neg(x529), pos(x83), x84)≥EVAL(neg(0), minus_int(neg(x529), x84), plus_int(pos(x83), neg(x529)), x84) ⇒ COND_EVAL1(true, neg(0), neg(s(x529)), pos(x83), x84)≥EVAL(neg(0), minus_int(neg(s(x529)), x84), plus_int(pos(x83), neg(s(x529))), x84))
(75) (COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(x90, x90), x90), x89)), neg(0), x89, x90, x91)=COND_EVAL1(true, x92, x93, neg(x94), x95) ⇒ COND_EVAL1(true, x92, x93, neg(x94), x95)≥EVAL(x92, minus_int(x93, x95), plus_int(neg(x94), x93), x95))
(76) (true=x533∧greatereq_int(x535, x89)=x534∧and(x533, x534)=true ⇒ COND_EVAL1(true, neg(0), x89, neg(x94), x91)≥EVAL(neg(0), minus_int(x89, x91), plus_int(neg(x94), x89), x91))
(77) (true=true∧greatereq_int(x535, x89)=true ⇒ COND_EVAL1(true, neg(0), x89, neg(x94), x91)≥EVAL(neg(0), minus_int(x89, x91), plus_int(neg(x94), x89), x91))
(78) (greatereq_int(x535, x89)=true ⇒ COND_EVAL1(true, neg(0), x89, neg(x94), x91)≥EVAL(neg(0), minus_int(x89, x91), plus_int(neg(x94), x89), x91))
(79) (true=true ⇒ COND_EVAL1(true, neg(0), pos(0), neg(x94), x91)≥EVAL(neg(0), minus_int(pos(0), x91), plus_int(neg(x94), pos(0)), x91))
(80) (true=true ⇒ COND_EVAL1(true, neg(0), pos(0), neg(x94), x91)≥EVAL(neg(0), minus_int(pos(0), x91), plus_int(neg(x94), pos(0)), x91))
(81) (true=true ⇒ COND_EVAL1(true, neg(0), neg(x542), neg(x94), x91)≥EVAL(neg(0), minus_int(neg(x542), x91), plus_int(neg(x94), neg(x542)), x91))
(82) (true=true ⇒ COND_EVAL1(true, neg(0), neg(x543), neg(x94), x91)≥EVAL(neg(0), minus_int(neg(x543), x91), plus_int(neg(x94), neg(x543)), x91))
(83) (greatereq_int(pos(x550), pos(x549))=true∧(∀x551,x552:greatereq_int(pos(x550), pos(x549))=true ⇒ COND_EVAL1(true, neg(0), pos(x549), neg(x551), x552)≥EVAL(neg(0), minus_int(pos(x549), x552), plus_int(neg(x551), pos(x549)), x552)) ⇒ COND_EVAL1(true, neg(0), pos(s(x549)), neg(x94), x91)≥EVAL(neg(0), minus_int(pos(s(x549)), x91), plus_int(neg(x94), pos(s(x549))), x91))
(84) (greatereq_int(neg(x554), neg(x553))=true∧(∀x555,x556:greatereq_int(neg(x554), neg(x553))=true ⇒ COND_EVAL1(true, neg(0), neg(x553), neg(x555), x556)≥EVAL(neg(0), minus_int(neg(x553), x556), plus_int(neg(x555), neg(x553)), x556)) ⇒ COND_EVAL1(true, neg(0), neg(s(x553)), neg(x94), x91)≥EVAL(neg(0), minus_int(neg(s(x553)), x91), plus_int(neg(x94), neg(s(x553))), x91))
(85) (COND_EVAL1(true, neg(0), pos(0), neg(x94), x91)≥EVAL(neg(0), minus_int(pos(0), x91), plus_int(neg(x94), pos(0)), x91))
(86) (COND_EVAL1(true, neg(0), pos(0), neg(x94), x91)≥EVAL(neg(0), minus_int(pos(0), x91), plus_int(neg(x94), pos(0)), x91))
(87) (COND_EVAL1(true, neg(0), neg(x542), neg(x94), x91)≥EVAL(neg(0), minus_int(neg(x542), x91), plus_int(neg(x94), neg(x542)), x91))
(88) (COND_EVAL1(true, neg(0), neg(x543), neg(x94), x91)≥EVAL(neg(0), minus_int(neg(x543), x91), plus_int(neg(x94), neg(x543)), x91))
(89) (COND_EVAL1(true, neg(0), pos(x549), neg(x94), x91)≥EVAL(neg(0), minus_int(pos(x549), x91), plus_int(neg(x94), pos(x549)), x91) ⇒ COND_EVAL1(true, neg(0), pos(s(x549)), neg(x94), x91)≥EVAL(neg(0), minus_int(pos(s(x549)), x91), plus_int(neg(x94), pos(s(x549))), x91))
(90) (COND_EVAL1(true, neg(0), neg(x553), neg(x94), x91)≥EVAL(neg(0), minus_int(neg(x553), x91), plus_int(neg(x94), neg(x553)), x91) ⇒ COND_EVAL1(true, neg(0), neg(s(x553)), neg(x94), x91)≥EVAL(neg(0), minus_int(neg(s(x553)), x91), plus_int(neg(x94), neg(s(x553))), x91))
(91) (COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(x109, x109), x109), x108)), pos(x107), x108, x109, x110)=COND_EVAL1(true, x111, x112, neg(x113), x114) ⇒ COND_EVAL1(true, x111, x112, neg(x113), x114)≥EVAL(x111, minus_int(x112, x114), plus_int(neg(x113), x112), x114))
(92) (true=x557∧greatereq_int(x559, x108)=x558∧and(x557, x558)=true ⇒ COND_EVAL1(true, pos(x107), x108, neg(x113), x110)≥EVAL(pos(x107), minus_int(x108, x110), plus_int(neg(x113), x108), x110))
(93) (true=true∧greatereq_int(x559, x108)=true ⇒ COND_EVAL1(true, pos(x107), x108, neg(x113), x110)≥EVAL(pos(x107), minus_int(x108, x110), plus_int(neg(x113), x108), x110))
(94) (greatereq_int(x559, x108)=true ⇒ COND_EVAL1(true, pos(x107), x108, neg(x113), x110)≥EVAL(pos(x107), minus_int(x108, x110), plus_int(neg(x113), x108), x110))
(95) (true=true ⇒ COND_EVAL1(true, pos(x107), pos(0), neg(x113), x110)≥EVAL(pos(x107), minus_int(pos(0), x110), plus_int(neg(x113), pos(0)), x110))
(96) (true=true ⇒ COND_EVAL1(true, pos(x107), pos(0), neg(x113), x110)≥EVAL(pos(x107), minus_int(pos(0), x110), plus_int(neg(x113), pos(0)), x110))
(97) (true=true ⇒ COND_EVAL1(true, pos(x107), neg(x566), neg(x113), x110)≥EVAL(pos(x107), minus_int(neg(x566), x110), plus_int(neg(x113), neg(x566)), x110))
(98) (true=true ⇒ COND_EVAL1(true, pos(x107), neg(x567), neg(x113), x110)≥EVAL(pos(x107), minus_int(neg(x567), x110), plus_int(neg(x113), neg(x567)), x110))
(99) (greatereq_int(pos(x574), pos(x573))=true∧(∀x575,x576,x577:greatereq_int(pos(x574), pos(x573))=true ⇒ COND_EVAL1(true, pos(x575), pos(x573), neg(x576), x577)≥EVAL(pos(x575), minus_int(pos(x573), x577), plus_int(neg(x576), pos(x573)), x577)) ⇒ COND_EVAL1(true, pos(x107), pos(s(x573)), neg(x113), x110)≥EVAL(pos(x107), minus_int(pos(s(x573)), x110), plus_int(neg(x113), pos(s(x573))), x110))
(100) (greatereq_int(neg(x579), neg(x578))=true∧(∀x580,x581,x582:greatereq_int(neg(x579), neg(x578))=true ⇒ COND_EVAL1(true, pos(x580), neg(x578), neg(x581), x582)≥EVAL(pos(x580), minus_int(neg(x578), x582), plus_int(neg(x581), neg(x578)), x582)) ⇒ COND_EVAL1(true, pos(x107), neg(s(x578)), neg(x113), x110)≥EVAL(pos(x107), minus_int(neg(s(x578)), x110), plus_int(neg(x113), neg(s(x578))), x110))
(101) (COND_EVAL1(true, pos(x107), pos(0), neg(x113), x110)≥EVAL(pos(x107), minus_int(pos(0), x110), plus_int(neg(x113), pos(0)), x110))
(102) (COND_EVAL1(true, pos(x107), pos(0), neg(x113), x110)≥EVAL(pos(x107), minus_int(pos(0), x110), plus_int(neg(x113), pos(0)), x110))
(103) (COND_EVAL1(true, pos(x107), neg(x566), neg(x113), x110)≥EVAL(pos(x107), minus_int(neg(x566), x110), plus_int(neg(x113), neg(x566)), x110))
(104) (COND_EVAL1(true, pos(x107), neg(x567), neg(x113), x110)≥EVAL(pos(x107), minus_int(neg(x567), x110), plus_int(neg(x113), neg(x567)), x110))
(105) (COND_EVAL1(true, pos(x107), pos(x573), neg(x113), x110)≥EVAL(pos(x107), minus_int(pos(x573), x110), plus_int(neg(x113), pos(x573)), x110) ⇒ COND_EVAL1(true, pos(x107), pos(s(x573)), neg(x113), x110)≥EVAL(pos(x107), minus_int(pos(s(x573)), x110), plus_int(neg(x113), pos(s(x573))), x110))
(106) (COND_EVAL1(true, pos(x107), neg(x578), neg(x113), x110)≥EVAL(pos(x107), minus_int(neg(x578), x110), plus_int(neg(x113), neg(x578)), x110) ⇒ COND_EVAL1(true, pos(x107), neg(s(x578)), neg(x113), x110)≥EVAL(pos(x107), minus_int(neg(s(x578)), x110), plus_int(neg(x113), neg(s(x578))), x110))
(107) (COND_EVAL1(and(greatereq_int(x119, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x121, x121), x121)), x120)), x119, x120, neg(x121), x122)=COND_EVAL1(true, x123, x124, neg(x125), x126) ⇒ COND_EVAL1(true, x123, x124, neg(x125), x126)≥EVAL(x123, minus_int(x124, x126), plus_int(neg(x125), x124), x126))
(108) (pos(0)=x585∧greatereq_int(x119, x585)=x583∧greatereq_int(x586, x120)=x584∧and(x583, x584)=true ⇒ COND_EVAL1(true, x119, x120, neg(x121), x122)≥EVAL(x119, minus_int(x120, x122), plus_int(neg(x121), x120), x122))
(109) (true=true∧pos(0)=x585∧greatereq_int(x119, x585)=true∧greatereq_int(x586, x120)=true ⇒ COND_EVAL1(true, x119, x120, neg(x121), x122)≥EVAL(x119, minus_int(x120, x122), plus_int(neg(x121), x120), x122))
(110) (pos(0)=x585∧greatereq_int(x119, x585)=true∧greatereq_int(x586, x120)=true ⇒ COND_EVAL1(true, x119, x120, neg(x121), x122)≥EVAL(x119, minus_int(x120, x122), plus_int(neg(x121), x120), x122))
(111) (true=true∧pos(0)=pos(0)∧greatereq_int(x586, x120)=true ⇒ COND_EVAL1(true, pos(x587), x120, neg(x121), x122)≥EVAL(pos(x587), minus_int(x120, x122), plus_int(neg(x121), x120), x122))
(112) (true=true∧pos(0)=pos(0)∧greatereq_int(x586, x120)=true ⇒ COND_EVAL1(true, neg(0), x120, neg(x121), x122)≥EVAL(neg(0), minus_int(x120, x122), plus_int(neg(x121), x120), x122))
(113) (true=true∧pos(0)=neg(x589)∧greatereq_int(x586, x120)=true ⇒ COND_EVAL1(true, neg(0), x120, neg(x121), x122)≥EVAL(neg(0), minus_int(x120, x122), plus_int(neg(x121), x120), x122))
(114) (true=true∧pos(0)=neg(x590)∧greatereq_int(x586, x120)=true ⇒ COND_EVAL1(true, pos(x591), x120, neg(x121), x122)≥EVAL(pos(x591), minus_int(x120, x122), plus_int(neg(x121), x120), x122))
(115) (greatereq_int(pos(x597), pos(x596))=true∧pos(0)=pos(s(x596))∧greatereq_int(x586, x120)=true∧(∀x598,x599,x600,x601:greatereq_int(pos(x597), pos(x596))=true∧pos(0)=pos(x596)∧greatereq_int(x598, x599)=true ⇒ COND_EVAL1(true, pos(x597), x599, neg(x600), x601)≥EVAL(pos(x597), minus_int(x599, x601), plus_int(neg(x600), x599), x601)) ⇒ COND_EVAL1(true, pos(s(x597)), x120, neg(x121), x122)≥EVAL(pos(s(x597)), minus_int(x120, x122), plus_int(neg(x121), x120), x122))
(116) (greatereq_int(neg(x603), neg(x602))=true∧pos(0)=neg(s(x602))∧greatereq_int(x586, x120)=true∧(∀x604,x605,x606,x607:greatereq_int(neg(x603), neg(x602))=true∧pos(0)=neg(x602)∧greatereq_int(x604, x605)=true ⇒ COND_EVAL1(true, neg(x603), x605, neg(x606), x607)≥EVAL(neg(x603), minus_int(x605, x607), plus_int(neg(x606), x605), x607)) ⇒ COND_EVAL1(true, neg(s(x603)), x120, neg(x121), x122)≥EVAL(neg(s(x603)), minus_int(x120, x122), plus_int(neg(x121), x120), x122))
(117) (greatereq_int(x586, x120)=true ⇒ COND_EVAL1(true, pos(x587), x120, neg(x121), x122)≥EVAL(pos(x587), minus_int(x120, x122), plus_int(neg(x121), x120), x122))
(118) (greatereq_int(x586, x120)=true ⇒ COND_EVAL1(true, neg(0), x120, neg(x121), x122)≥EVAL(neg(0), minus_int(x120, x122), plus_int(neg(x121), x120), x122))
(119) (true=true ⇒ COND_EVAL1(true, pos(x587), pos(0), neg(x121), x122)≥EVAL(pos(x587), minus_int(pos(0), x122), plus_int(neg(x121), pos(0)), x122))
(120) (true=true ⇒ COND_EVAL1(true, pos(x587), pos(0), neg(x121), x122)≥EVAL(pos(x587), minus_int(pos(0), x122), plus_int(neg(x121), pos(0)), x122))
(121) (true=true ⇒ COND_EVAL1(true, pos(x587), neg(x610), neg(x121), x122)≥EVAL(pos(x587), minus_int(neg(x610), x122), plus_int(neg(x121), neg(x610)), x122))
(122) (true=true ⇒ COND_EVAL1(true, pos(x587), neg(x611), neg(x121), x122)≥EVAL(pos(x587), minus_int(neg(x611), x122), plus_int(neg(x121), neg(x611)), x122))
(123) (greatereq_int(pos(x618), pos(x617))=true∧(∀x619,x620,x621:greatereq_int(pos(x618), pos(x617))=true ⇒ COND_EVAL1(true, pos(x619), pos(x617), neg(x620), x621)≥EVAL(pos(x619), minus_int(pos(x617), x621), plus_int(neg(x620), pos(x617)), x621)) ⇒ COND_EVAL1(true, pos(x587), pos(s(x617)), neg(x121), x122)≥EVAL(pos(x587), minus_int(pos(s(x617)), x122), plus_int(neg(x121), pos(s(x617))), x122))
(124) (greatereq_int(neg(x623), neg(x622))=true∧(∀x624,x625,x626:greatereq_int(neg(x623), neg(x622))=true ⇒ COND_EVAL1(true, pos(x624), neg(x622), neg(x625), x626)≥EVAL(pos(x624), minus_int(neg(x622), x626), plus_int(neg(x625), neg(x622)), x626)) ⇒ COND_EVAL1(true, pos(x587), neg(s(x622)), neg(x121), x122)≥EVAL(pos(x587), minus_int(neg(s(x622)), x122), plus_int(neg(x121), neg(s(x622))), x122))
(125) (COND_EVAL1(true, pos(x587), pos(0), neg(x121), x122)≥EVAL(pos(x587), minus_int(pos(0), x122), plus_int(neg(x121), pos(0)), x122))
(126) (COND_EVAL1(true, pos(x587), pos(0), neg(x121), x122)≥EVAL(pos(x587), minus_int(pos(0), x122), plus_int(neg(x121), pos(0)), x122))
(127) (COND_EVAL1(true, pos(x587), neg(x610), neg(x121), x122)≥EVAL(pos(x587), minus_int(neg(x610), x122), plus_int(neg(x121), neg(x610)), x122))
(128) (COND_EVAL1(true, pos(x587), neg(x611), neg(x121), x122)≥EVAL(pos(x587), minus_int(neg(x611), x122), plus_int(neg(x121), neg(x611)), x122))
(129) (COND_EVAL1(true, pos(x587), pos(x617), neg(x121), x122)≥EVAL(pos(x587), minus_int(pos(x617), x122), plus_int(neg(x121), pos(x617)), x122) ⇒ COND_EVAL1(true, pos(x587), pos(s(x617)), neg(x121), x122)≥EVAL(pos(x587), minus_int(pos(s(x617)), x122), plus_int(neg(x121), pos(s(x617))), x122))
(130) (COND_EVAL1(true, pos(x587), neg(x622), neg(x121), x122)≥EVAL(pos(x587), minus_int(neg(x622), x122), plus_int(neg(x121), neg(x622)), x122) ⇒ COND_EVAL1(true, pos(x587), neg(s(x622)), neg(x121), x122)≥EVAL(pos(x587), minus_int(neg(s(x622)), x122), plus_int(neg(x121), neg(s(x622))), x122))
(131) (true=true ⇒ COND_EVAL1(true, neg(0), pos(0), neg(x121), x122)≥EVAL(neg(0), minus_int(pos(0), x122), plus_int(neg(x121), pos(0)), x122))
(132) (true=true ⇒ COND_EVAL1(true, neg(0), pos(0), neg(x121), x122)≥EVAL(neg(0), minus_int(pos(0), x122), plus_int(neg(x121), pos(0)), x122))
(133) (true=true ⇒ COND_EVAL1(true, neg(0), neg(x629), neg(x121), x122)≥EVAL(neg(0), minus_int(neg(x629), x122), plus_int(neg(x121), neg(x629)), x122))
(134) (true=true ⇒ COND_EVAL1(true, neg(0), neg(x630), neg(x121), x122)≥EVAL(neg(0), minus_int(neg(x630), x122), plus_int(neg(x121), neg(x630)), x122))
(135) (greatereq_int(pos(x637), pos(x636))=true∧(∀x638,x639:greatereq_int(pos(x637), pos(x636))=true ⇒ COND_EVAL1(true, neg(0), pos(x636), neg(x638), x639)≥EVAL(neg(0), minus_int(pos(x636), x639), plus_int(neg(x638), pos(x636)), x639)) ⇒ COND_EVAL1(true, neg(0), pos(s(x636)), neg(x121), x122)≥EVAL(neg(0), minus_int(pos(s(x636)), x122), plus_int(neg(x121), pos(s(x636))), x122))
(136) (greatereq_int(neg(x641), neg(x640))=true∧(∀x642,x643:greatereq_int(neg(x641), neg(x640))=true ⇒ COND_EVAL1(true, neg(0), neg(x640), neg(x642), x643)≥EVAL(neg(0), minus_int(neg(x640), x643), plus_int(neg(x642), neg(x640)), x643)) ⇒ COND_EVAL1(true, neg(0), neg(s(x640)), neg(x121), x122)≥EVAL(neg(0), minus_int(neg(s(x640)), x122), plus_int(neg(x121), neg(s(x640))), x122))
(137) (COND_EVAL1(true, neg(0), pos(0), neg(x121), x122)≥EVAL(neg(0), minus_int(pos(0), x122), plus_int(neg(x121), pos(0)), x122))
(138) (COND_EVAL1(true, neg(0), pos(0), neg(x121), x122)≥EVAL(neg(0), minus_int(pos(0), x122), plus_int(neg(x121), pos(0)), x122))
(139) (COND_EVAL1(true, neg(0), neg(x629), neg(x121), x122)≥EVAL(neg(0), minus_int(neg(x629), x122), plus_int(neg(x121), neg(x629)), x122))
(140) (COND_EVAL1(true, neg(0), neg(x630), neg(x121), x122)≥EVAL(neg(0), minus_int(neg(x630), x122), plus_int(neg(x121), neg(x630)), x122))
(141) (COND_EVAL1(true, neg(0), pos(x636), neg(x121), x122)≥EVAL(neg(0), minus_int(pos(x636), x122), plus_int(neg(x121), pos(x636)), x122) ⇒ COND_EVAL1(true, neg(0), pos(s(x636)), neg(x121), x122)≥EVAL(neg(0), minus_int(pos(s(x636)), x122), plus_int(neg(x121), pos(s(x636))), x122))
(142) (COND_EVAL1(true, neg(0), neg(x640), neg(x121), x122)≥EVAL(neg(0), minus_int(neg(x640), x122), plus_int(neg(x121), neg(x640)), x122) ⇒ COND_EVAL1(true, neg(0), neg(s(x640)), neg(x121), x122)≥EVAL(neg(0), minus_int(neg(s(x640)), x122), plus_int(neg(x121), neg(s(x640))), x122))
(143) (COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(x136, x136), x136), x135)), neg(0), x135, x136, x137)=COND_EVAL1(true, neg(0), x138, x139, x140) ⇒ COND_EVAL1(true, neg(0), x138, x139, x140)≥EVAL(neg(0), minus_int(x138, x140), plus_int(x139, x138), x140))
(144) (true=x644∧greatereq_int(x646, x135)=x645∧and(x644, x645)=true ⇒ COND_EVAL1(true, neg(0), x135, x136, x137)≥EVAL(neg(0), minus_int(x135, x137), plus_int(x136, x135), x137))
(145) (true=true∧greatereq_int(x646, x135)=true ⇒ COND_EVAL1(true, neg(0), x135, x136, x137)≥EVAL(neg(0), minus_int(x135, x137), plus_int(x136, x135), x137))
(146) (greatereq_int(x646, x135)=true ⇒ COND_EVAL1(true, neg(0), x135, x136, x137)≥EVAL(neg(0), minus_int(x135, x137), plus_int(x136, x135), x137))
(147) (true=true ⇒ COND_EVAL1(true, neg(0), pos(0), x136, x137)≥EVAL(neg(0), minus_int(pos(0), x137), plus_int(x136, pos(0)), x137))
(148) (true=true ⇒ COND_EVAL1(true, neg(0), pos(0), x136, x137)≥EVAL(neg(0), minus_int(pos(0), x137), plus_int(x136, pos(0)), x137))
(149) (true=true ⇒ COND_EVAL1(true, neg(0), neg(x651), x136, x137)≥EVAL(neg(0), minus_int(neg(x651), x137), plus_int(x136, neg(x651)), x137))
(150) (true=true ⇒ COND_EVAL1(true, neg(0), neg(x652), x136, x137)≥EVAL(neg(0), minus_int(neg(x652), x137), plus_int(x136, neg(x652)), x137))
(151) (greatereq_int(pos(x659), pos(x658))=true∧(∀x660,x661:greatereq_int(pos(x659), pos(x658))=true ⇒ COND_EVAL1(true, neg(0), pos(x658), x660, x661)≥EVAL(neg(0), minus_int(pos(x658), x661), plus_int(x660, pos(x658)), x661)) ⇒ COND_EVAL1(true, neg(0), pos(s(x658)), x136, x137)≥EVAL(neg(0), minus_int(pos(s(x658)), x137), plus_int(x136, pos(s(x658))), x137))
(152) (greatereq_int(neg(x663), neg(x662))=true∧(∀x664,x665:greatereq_int(neg(x663), neg(x662))=true ⇒ COND_EVAL1(true, neg(0), neg(x662), x664, x665)≥EVAL(neg(0), minus_int(neg(x662), x665), plus_int(x664, neg(x662)), x665)) ⇒ COND_EVAL1(true, neg(0), neg(s(x662)), x136, x137)≥EVAL(neg(0), minus_int(neg(s(x662)), x137), plus_int(x136, neg(s(x662))), x137))
(153) (COND_EVAL1(true, neg(0), pos(0), x136, x137)≥EVAL(neg(0), minus_int(pos(0), x137), plus_int(x136, pos(0)), x137))
(154) (COND_EVAL1(true, neg(0), pos(0), x136, x137)≥EVAL(neg(0), minus_int(pos(0), x137), plus_int(x136, pos(0)), x137))
(155) (COND_EVAL1(true, neg(0), neg(x651), x136, x137)≥EVAL(neg(0), minus_int(neg(x651), x137), plus_int(x136, neg(x651)), x137))
(156) (COND_EVAL1(true, neg(0), neg(x652), x136, x137)≥EVAL(neg(0), minus_int(neg(x652), x137), plus_int(x136, neg(x652)), x137))
(157) (COND_EVAL1(true, neg(0), pos(x658), x136, x137)≥EVAL(neg(0), minus_int(pos(x658), x137), plus_int(x136, pos(x658)), x137) ⇒ COND_EVAL1(true, neg(0), pos(s(x658)), x136, x137)≥EVAL(neg(0), minus_int(pos(s(x658)), x137), plus_int(x136, pos(s(x658))), x137))
(158) (COND_EVAL1(true, neg(0), neg(x662), x136, x137)≥EVAL(neg(0), minus_int(neg(x662), x137), plus_int(x136, neg(x662)), x137) ⇒ COND_EVAL1(true, neg(0), neg(s(x662)), x136, x137)≥EVAL(neg(0), minus_int(neg(s(x662)), x137), plus_int(x136, neg(s(x662))), x137))
(159) (COND_EVAL1(and(greatereq_int(x160, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x162, x162), x162)), x161)), x160, x161, neg(x162), x163)=COND_EVAL1(true, neg(0), x164, x165, x166) ⇒ COND_EVAL1(true, neg(0), x164, x165, x166)≥EVAL(neg(0), minus_int(x164, x166), plus_int(x165, x164), x166))
(160) (neg(0)=x668∧pos(0)=x669∧greatereq_int(x668, x669)=x666∧greatereq_int(x670, x161)=x667∧and(x666, x667)=true ⇒ COND_EVAL1(true, neg(0), x161, neg(x162), x163)≥EVAL(neg(0), minus_int(x161, x163), plus_int(neg(x162), x161), x163))
(161) (true=true∧neg(0)=x668∧pos(0)=x669∧greatereq_int(x668, x669)=true∧greatereq_int(x670, x161)=true ⇒ COND_EVAL1(true, neg(0), x161, neg(x162), x163)≥EVAL(neg(0), minus_int(x161, x163), plus_int(neg(x162), x161), x163))
(162) (neg(0)=x668∧pos(0)=x669∧greatereq_int(x668, x669)=true∧greatereq_int(x670, x161)=true ⇒ COND_EVAL1(true, neg(0), x161, neg(x162), x163)≥EVAL(neg(0), minus_int(x161, x163), plus_int(neg(x162), x161), x163))
(163) (true=true∧neg(0)=pos(x671)∧pos(0)=pos(0)∧greatereq_int(x670, x161)=true ⇒ COND_EVAL1(true, neg(0), x161, neg(x162), x163)≥EVAL(neg(0), minus_int(x161, x163), plus_int(neg(x162), x161), x163))
(164) (true=true∧neg(0)=neg(0)∧pos(0)=pos(0)∧greatereq_int(x670, x161)=true ⇒ COND_EVAL1(true, neg(0), x161, neg(x162), x163)≥EVAL(neg(0), minus_int(x161, x163), plus_int(neg(x162), x161), x163))
(165) (true=true∧neg(0)=neg(0)∧pos(0)=neg(x673)∧greatereq_int(x670, x161)=true ⇒ COND_EVAL1(true, neg(0), x161, neg(x162), x163)≥EVAL(neg(0), minus_int(x161, x163), plus_int(neg(x162), x161), x163))
(166) (true=true∧neg(0)=pos(x675)∧pos(0)=neg(x674)∧greatereq_int(x670, x161)=true ⇒ COND_EVAL1(true, neg(0), x161, neg(x162), x163)≥EVAL(neg(0), minus_int(x161, x163), plus_int(neg(x162), x161), x163))
(167) (greatereq_int(pos(x681), pos(x680))=true∧neg(0)=pos(s(x681))∧pos(0)=pos(s(x680))∧greatereq_int(x670, x161)=true∧(∀x682,x683,x684,x685:greatereq_int(pos(x681), pos(x680))=true∧neg(0)=pos(x681)∧pos(0)=pos(x680)∧greatereq_int(x682, x683)=true ⇒ COND_EVAL1(true, neg(0), x683, neg(x684), x685)≥EVAL(neg(0), minus_int(x683, x685), plus_int(neg(x684), x683), x685)) ⇒ COND_EVAL1(true, neg(0), x161, neg(x162), x163)≥EVAL(neg(0), minus_int(x161, x163), plus_int(neg(x162), x161), x163))
(168) (greatereq_int(neg(x687), neg(x686))=true∧neg(0)=neg(s(x687))∧pos(0)=neg(s(x686))∧greatereq_int(x670, x161)=true∧(∀x688,x689,x690,x691:greatereq_int(neg(x687), neg(x686))=true∧neg(0)=neg(x687)∧pos(0)=neg(x686)∧greatereq_int(x688, x689)=true ⇒ COND_EVAL1(true, neg(0), x689, neg(x690), x691)≥EVAL(neg(0), minus_int(x689, x691), plus_int(neg(x690), x689), x691)) ⇒ COND_EVAL1(true, neg(0), x161, neg(x162), x163)≥EVAL(neg(0), minus_int(x161, x163), plus_int(neg(x162), x161), x163))
(169) (greatereq_int(x670, x161)=true ⇒ COND_EVAL1(true, neg(0), x161, neg(x162), x163)≥EVAL(neg(0), minus_int(x161, x163), plus_int(neg(x162), x161), x163))
(170) (true=true ⇒ COND_EVAL1(true, neg(0), pos(0), neg(x162), x163)≥EVAL(neg(0), minus_int(pos(0), x163), plus_int(neg(x162), pos(0)), x163))
(171) (true=true ⇒ COND_EVAL1(true, neg(0), pos(0), neg(x162), x163)≥EVAL(neg(0), minus_int(pos(0), x163), plus_int(neg(x162), pos(0)), x163))
(172) (true=true ⇒ COND_EVAL1(true, neg(0), neg(x694), neg(x162), x163)≥EVAL(neg(0), minus_int(neg(x694), x163), plus_int(neg(x162), neg(x694)), x163))
(173) (true=true ⇒ COND_EVAL1(true, neg(0), neg(x695), neg(x162), x163)≥EVAL(neg(0), minus_int(neg(x695), x163), plus_int(neg(x162), neg(x695)), x163))
(174) (greatereq_int(pos(x702), pos(x701))=true∧(∀x703,x704:greatereq_int(pos(x702), pos(x701))=true ⇒ COND_EVAL1(true, neg(0), pos(x701), neg(x703), x704)≥EVAL(neg(0), minus_int(pos(x701), x704), plus_int(neg(x703), pos(x701)), x704)) ⇒ COND_EVAL1(true, neg(0), pos(s(x701)), neg(x162), x163)≥EVAL(neg(0), minus_int(pos(s(x701)), x163), plus_int(neg(x162), pos(s(x701))), x163))
(175) (greatereq_int(neg(x706), neg(x705))=true∧(∀x707,x708:greatereq_int(neg(x706), neg(x705))=true ⇒ COND_EVAL1(true, neg(0), neg(x705), neg(x707), x708)≥EVAL(neg(0), minus_int(neg(x705), x708), plus_int(neg(x707), neg(x705)), x708)) ⇒ COND_EVAL1(true, neg(0), neg(s(x705)), neg(x162), x163)≥EVAL(neg(0), minus_int(neg(s(x705)), x163), plus_int(neg(x162), neg(s(x705))), x163))
(176) (COND_EVAL1(true, neg(0), pos(0), neg(x162), x163)≥EVAL(neg(0), minus_int(pos(0), x163), plus_int(neg(x162), pos(0)), x163))
(177) (COND_EVAL1(true, neg(0), pos(0), neg(x162), x163)≥EVAL(neg(0), minus_int(pos(0), x163), plus_int(neg(x162), pos(0)), x163))
(178) (COND_EVAL1(true, neg(0), neg(x694), neg(x162), x163)≥EVAL(neg(0), minus_int(neg(x694), x163), plus_int(neg(x162), neg(x694)), x163))
(179) (COND_EVAL1(true, neg(0), neg(x695), neg(x162), x163)≥EVAL(neg(0), minus_int(neg(x695), x163), plus_int(neg(x162), neg(x695)), x163))
(180) (COND_EVAL1(true, neg(0), pos(x701), neg(x162), x163)≥EVAL(neg(0), minus_int(pos(x701), x163), plus_int(neg(x162), pos(x701)), x163) ⇒ COND_EVAL1(true, neg(0), pos(s(x701)), neg(x162), x163)≥EVAL(neg(0), minus_int(pos(s(x701)), x163), plus_int(neg(x162), pos(s(x701))), x163))
(181) (COND_EVAL1(true, neg(0), neg(x705), neg(x162), x163)≥EVAL(neg(0), minus_int(neg(x705), x163), plus_int(neg(x162), neg(x705)), x163) ⇒ COND_EVAL1(true, neg(0), neg(s(x705)), neg(x162), x163)≥EVAL(neg(0), minus_int(neg(s(x705)), x163), plus_int(neg(x162), neg(s(x705))), x163))
(182) (COND_EVAL1(and(greatereq_int(x171, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x173, x173), x173)), x172)), x171, x172, pos(x173), x174)=COND_EVAL1(true, neg(0), x175, x176, x177) ⇒ COND_EVAL1(true, neg(0), x175, x176, x177)≥EVAL(neg(0), minus_int(x175, x177), plus_int(x176, x175), x177))
(183) (neg(0)=x711∧pos(0)=x712∧greatereq_int(x711, x712)=x709∧greatereq_int(x713, x172)=x710∧and(x709, x710)=true ⇒ COND_EVAL1(true, neg(0), x172, pos(x173), x174)≥EVAL(neg(0), minus_int(x172, x174), plus_int(pos(x173), x172), x174))
(184) (true=true∧neg(0)=x711∧pos(0)=x712∧greatereq_int(x711, x712)=true∧greatereq_int(x713, x172)=true ⇒ COND_EVAL1(true, neg(0), x172, pos(x173), x174)≥EVAL(neg(0), minus_int(x172, x174), plus_int(pos(x173), x172), x174))
(185) (neg(0)=x711∧pos(0)=x712∧greatereq_int(x711, x712)=true∧greatereq_int(x713, x172)=true ⇒ COND_EVAL1(true, neg(0), x172, pos(x173), x174)≥EVAL(neg(0), minus_int(x172, x174), plus_int(pos(x173), x172), x174))
(186) (true=true∧neg(0)=pos(x714)∧pos(0)=pos(0)∧greatereq_int(x713, x172)=true ⇒ COND_EVAL1(true, neg(0), x172, pos(x173), x174)≥EVAL(neg(0), minus_int(x172, x174), plus_int(pos(x173), x172), x174))
(187) (true=true∧neg(0)=neg(0)∧pos(0)=pos(0)∧greatereq_int(x713, x172)=true ⇒ COND_EVAL1(true, neg(0), x172, pos(x173), x174)≥EVAL(neg(0), minus_int(x172, x174), plus_int(pos(x173), x172), x174))
(188) (true=true∧neg(0)=neg(0)∧pos(0)=neg(x716)∧greatereq_int(x713, x172)=true ⇒ COND_EVAL1(true, neg(0), x172, pos(x173), x174)≥EVAL(neg(0), minus_int(x172, x174), plus_int(pos(x173), x172), x174))
(189) (true=true∧neg(0)=pos(x718)∧pos(0)=neg(x717)∧greatereq_int(x713, x172)=true ⇒ COND_EVAL1(true, neg(0), x172, pos(x173), x174)≥EVAL(neg(0), minus_int(x172, x174), plus_int(pos(x173), x172), x174))
(190) (greatereq_int(pos(x724), pos(x723))=true∧neg(0)=pos(s(x724))∧pos(0)=pos(s(x723))∧greatereq_int(x713, x172)=true∧(∀x725,x726,x727,x728:greatereq_int(pos(x724), pos(x723))=true∧neg(0)=pos(x724)∧pos(0)=pos(x723)∧greatereq_int(x725, x726)=true ⇒ COND_EVAL1(true, neg(0), x726, pos(x727), x728)≥EVAL(neg(0), minus_int(x726, x728), plus_int(pos(x727), x726), x728)) ⇒ COND_EVAL1(true, neg(0), x172, pos(x173), x174)≥EVAL(neg(0), minus_int(x172, x174), plus_int(pos(x173), x172), x174))
(191) (greatereq_int(neg(x730), neg(x729))=true∧neg(0)=neg(s(x730))∧pos(0)=neg(s(x729))∧greatereq_int(x713, x172)=true∧(∀x731,x732,x733,x734:greatereq_int(neg(x730), neg(x729))=true∧neg(0)=neg(x730)∧pos(0)=neg(x729)∧greatereq_int(x731, x732)=true ⇒ COND_EVAL1(true, neg(0), x732, pos(x733), x734)≥EVAL(neg(0), minus_int(x732, x734), plus_int(pos(x733), x732), x734)) ⇒ COND_EVAL1(true, neg(0), x172, pos(x173), x174)≥EVAL(neg(0), minus_int(x172, x174), plus_int(pos(x173), x172), x174))
(192) (greatereq_int(x713, x172)=true ⇒ COND_EVAL1(true, neg(0), x172, pos(x173), x174)≥EVAL(neg(0), minus_int(x172, x174), plus_int(pos(x173), x172), x174))
(193) (true=true ⇒ COND_EVAL1(true, neg(0), pos(0), pos(x173), x174)≥EVAL(neg(0), minus_int(pos(0), x174), plus_int(pos(x173), pos(0)), x174))
(194) (true=true ⇒ COND_EVAL1(true, neg(0), pos(0), pos(x173), x174)≥EVAL(neg(0), minus_int(pos(0), x174), plus_int(pos(x173), pos(0)), x174))
(195) (true=true ⇒ COND_EVAL1(true, neg(0), neg(x737), pos(x173), x174)≥EVAL(neg(0), minus_int(neg(x737), x174), plus_int(pos(x173), neg(x737)), x174))
(196) (true=true ⇒ COND_EVAL1(true, neg(0), neg(x738), pos(x173), x174)≥EVAL(neg(0), minus_int(neg(x738), x174), plus_int(pos(x173), neg(x738)), x174))
(197) (greatereq_int(pos(x745), pos(x744))=true∧(∀x746,x747:greatereq_int(pos(x745), pos(x744))=true ⇒ COND_EVAL1(true, neg(0), pos(x744), pos(x746), x747)≥EVAL(neg(0), minus_int(pos(x744), x747), plus_int(pos(x746), pos(x744)), x747)) ⇒ COND_EVAL1(true, neg(0), pos(s(x744)), pos(x173), x174)≥EVAL(neg(0), minus_int(pos(s(x744)), x174), plus_int(pos(x173), pos(s(x744))), x174))
(198) (greatereq_int(neg(x749), neg(x748))=true∧(∀x750,x751:greatereq_int(neg(x749), neg(x748))=true ⇒ COND_EVAL1(true, neg(0), neg(x748), pos(x750), x751)≥EVAL(neg(0), minus_int(neg(x748), x751), plus_int(pos(x750), neg(x748)), x751)) ⇒ COND_EVAL1(true, neg(0), neg(s(x748)), pos(x173), x174)≥EVAL(neg(0), minus_int(neg(s(x748)), x174), plus_int(pos(x173), neg(s(x748))), x174))
(199) (COND_EVAL1(true, neg(0), pos(0), pos(x173), x174)≥EVAL(neg(0), minus_int(pos(0), x174), plus_int(pos(x173), pos(0)), x174))
(200) (COND_EVAL1(true, neg(0), pos(0), pos(x173), x174)≥EVAL(neg(0), minus_int(pos(0), x174), plus_int(pos(x173), pos(0)), x174))
(201) (COND_EVAL1(true, neg(0), neg(x737), pos(x173), x174)≥EVAL(neg(0), minus_int(neg(x737), x174), plus_int(pos(x173), neg(x737)), x174))
(202) (COND_EVAL1(true, neg(0), neg(x738), pos(x173), x174)≥EVAL(neg(0), minus_int(neg(x738), x174), plus_int(pos(x173), neg(x738)), x174))
(203) (COND_EVAL1(true, neg(0), pos(x744), pos(x173), x174)≥EVAL(neg(0), minus_int(pos(x744), x174), plus_int(pos(x173), pos(x744)), x174) ⇒ COND_EVAL1(true, neg(0), pos(s(x744)), pos(x173), x174)≥EVAL(neg(0), minus_int(pos(s(x744)), x174), plus_int(pos(x173), pos(s(x744))), x174))
(204) (COND_EVAL1(true, neg(0), neg(x748), pos(x173), x174)≥EVAL(neg(0), minus_int(neg(x748), x174), plus_int(pos(x173), neg(x748)), x174) ⇒ COND_EVAL1(true, neg(0), neg(s(x748)), pos(x173), x174)≥EVAL(neg(0), minus_int(neg(s(x748)), x174), plus_int(pos(x173), neg(s(x748))), x174))
(205) (EVAL(x181, minus_int(x182, x184), plus_int(pos(x183), x182), x184)=EVAL(pos(x185), x186, x187, x188) ⇒ EVAL(pos(x185), x186, x187, x188)≥COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(x187, x187), x187), x186)), pos(x185), x186, x187, x188))
(206) (EVAL(pos(x185), x186, x187, x184)≥COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(x187, x187), x187), x186)), pos(x185), x186, x187, x184))
(207) (EVAL(x189, minus_int(x190, x192), plus_int(neg(x191), x190), x192)=EVAL(pos(x193), x194, x195, x196) ⇒ EVAL(pos(x193), x194, x195, x196)≥COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(x195, x195), x195), x194)), pos(x193), x194, x195, x196))
(208) (EVAL(pos(x193), x194, x195, x192)≥COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(x195, x195), x195), x194)), pos(x193), x194, x195, x192))
(209) (EVAL(pos(x204), minus_int(x205, x207), plus_int(x206, x205), x207)=EVAL(pos(x208), x209, x210, x211) ⇒ EVAL(pos(x208), x209, x210, x211)≥COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(x210, x210), x210), x209)), pos(x208), x209, x210, x211))
(210) (EVAL(pos(x204), x209, x210, x207)≥COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(x210, x210), x210), x209)), pos(x204), x209, x210, x207))
(211) (COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(x240, x240), x240), x239)), pos(x238), x239, x240, x241)=COND_EVAL1(true, pos(x242), x243, x244, x245) ⇒ COND_EVAL1(true, pos(x242), x243, x244, x245)≥EVAL(pos(x242), minus_int(x243, x245), plus_int(x244, x243), x245))
(212) (true=x754∧greatereq_int(x756, x239)=x755∧and(x754, x755)=true ⇒ COND_EVAL1(true, pos(x238), x239, x240, x241)≥EVAL(pos(x238), minus_int(x239, x241), plus_int(x240, x239), x241))
(213) (true=true∧greatereq_int(x756, x239)=true ⇒ COND_EVAL1(true, pos(x238), x239, x240, x241)≥EVAL(pos(x238), minus_int(x239, x241), plus_int(x240, x239), x241))
(214) (greatereq_int(x756, x239)=true ⇒ COND_EVAL1(true, pos(x238), x239, x240, x241)≥EVAL(pos(x238), minus_int(x239, x241), plus_int(x240, x239), x241))
(215) (true=true ⇒ COND_EVAL1(true, pos(x238), pos(0), x240, x241)≥EVAL(pos(x238), minus_int(pos(0), x241), plus_int(x240, pos(0)), x241))
(216) (true=true ⇒ COND_EVAL1(true, pos(x238), pos(0), x240, x241)≥EVAL(pos(x238), minus_int(pos(0), x241), plus_int(x240, pos(0)), x241))
(217) (true=true ⇒ COND_EVAL1(true, pos(x238), neg(x761), x240, x241)≥EVAL(pos(x238), minus_int(neg(x761), x241), plus_int(x240, neg(x761)), x241))
(218) (true=true ⇒ COND_EVAL1(true, pos(x238), neg(x762), x240, x241)≥EVAL(pos(x238), minus_int(neg(x762), x241), plus_int(x240, neg(x762)), x241))
(219) (greatereq_int(pos(x769), pos(x768))=true∧(∀x770,x771,x772:greatereq_int(pos(x769), pos(x768))=true ⇒ COND_EVAL1(true, pos(x770), pos(x768), x771, x772)≥EVAL(pos(x770), minus_int(pos(x768), x772), plus_int(x771, pos(x768)), x772)) ⇒ COND_EVAL1(true, pos(x238), pos(s(x768)), x240, x241)≥EVAL(pos(x238), minus_int(pos(s(x768)), x241), plus_int(x240, pos(s(x768))), x241))
(220) (greatereq_int(neg(x774), neg(x773))=true∧(∀x775,x776,x777:greatereq_int(neg(x774), neg(x773))=true ⇒ COND_EVAL1(true, pos(x775), neg(x773), x776, x777)≥EVAL(pos(x775), minus_int(neg(x773), x777), plus_int(x776, neg(x773)), x777)) ⇒ COND_EVAL1(true, pos(x238), neg(s(x773)), x240, x241)≥EVAL(pos(x238), minus_int(neg(s(x773)), x241), plus_int(x240, neg(s(x773))), x241))
(221) (COND_EVAL1(true, pos(x238), pos(0), x240, x241)≥EVAL(pos(x238), minus_int(pos(0), x241), plus_int(x240, pos(0)), x241))
(222) (COND_EVAL1(true, pos(x238), pos(0), x240, x241)≥EVAL(pos(x238), minus_int(pos(0), x241), plus_int(x240, pos(0)), x241))
(223) (COND_EVAL1(true, pos(x238), neg(x761), x240, x241)≥EVAL(pos(x238), minus_int(neg(x761), x241), plus_int(x240, neg(x761)), x241))
(224) (COND_EVAL1(true, pos(x238), neg(x762), x240, x241)≥EVAL(pos(x238), minus_int(neg(x762), x241), plus_int(x240, neg(x762)), x241))
(225) (COND_EVAL1(true, pos(x238), pos(x768), x240, x241)≥EVAL(pos(x238), minus_int(pos(x768), x241), plus_int(x240, pos(x768)), x241) ⇒ COND_EVAL1(true, pos(x238), pos(s(x768)), x240, x241)≥EVAL(pos(x238), minus_int(pos(s(x768)), x241), plus_int(x240, pos(s(x768))), x241))
(226) (COND_EVAL1(true, pos(x238), neg(x773), x240, x241)≥EVAL(pos(x238), minus_int(neg(x773), x241), plus_int(x240, neg(x773)), x241) ⇒ COND_EVAL1(true, pos(x238), neg(s(x773)), x240, x241)≥EVAL(pos(x238), minus_int(neg(s(x773)), x241), plus_int(x240, neg(s(x773))), x241))
(227) (COND_EVAL1(and(greatereq_int(x250, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x252, x252), x252)), x251)), x250, x251, neg(x252), x253)=COND_EVAL1(true, pos(x254), x255, x256, x257) ⇒ COND_EVAL1(true, pos(x254), x255, x256, x257)≥EVAL(pos(x254), minus_int(x255, x257), plus_int(x256, x255), x257))
(228) (pos(x254)=x780∧pos(0)=x781∧greatereq_int(x780, x781)=x778∧greatereq_int(x782, x251)=x779∧and(x778, x779)=true ⇒ COND_EVAL1(true, pos(x254), x251, neg(x252), x253)≥EVAL(pos(x254), minus_int(x251, x253), plus_int(neg(x252), x251), x253))
(229) (true=true∧pos(x254)=x780∧pos(0)=x781∧greatereq_int(x780, x781)=true∧greatereq_int(x782, x251)=true ⇒ COND_EVAL1(true, pos(x254), x251, neg(x252), x253)≥EVAL(pos(x254), minus_int(x251, x253), plus_int(neg(x252), x251), x253))
(230) (pos(x254)=x780∧pos(0)=x781∧greatereq_int(x780, x781)=true∧greatereq_int(x782, x251)=true ⇒ COND_EVAL1(true, pos(x254), x251, neg(x252), x253)≥EVAL(pos(x254), minus_int(x251, x253), plus_int(neg(x252), x251), x253))
(231) (true=true∧pos(x254)=pos(x783)∧pos(0)=pos(0)∧greatereq_int(x782, x251)=true ⇒ COND_EVAL1(true, pos(x254), x251, neg(x252), x253)≥EVAL(pos(x254), minus_int(x251, x253), plus_int(neg(x252), x251), x253))
(232) (true=true∧pos(x254)=neg(0)∧pos(0)=pos(0)∧greatereq_int(x782, x251)=true ⇒ COND_EVAL1(true, pos(x254), x251, neg(x252), x253)≥EVAL(pos(x254), minus_int(x251, x253), plus_int(neg(x252), x251), x253))
(233) (true=true∧pos(x254)=neg(0)∧pos(0)=neg(x785)∧greatereq_int(x782, x251)=true ⇒ COND_EVAL1(true, pos(x254), x251, neg(x252), x253)≥EVAL(pos(x254), minus_int(x251, x253), plus_int(neg(x252), x251), x253))
(234) (true=true∧pos(x254)=pos(x787)∧pos(0)=neg(x786)∧greatereq_int(x782, x251)=true ⇒ COND_EVAL1(true, pos(x254), x251, neg(x252), x253)≥EVAL(pos(x254), minus_int(x251, x253), plus_int(neg(x252), x251), x253))
(235) (greatereq_int(pos(x793), pos(x792))=true∧pos(x254)=pos(s(x793))∧pos(0)=pos(s(x792))∧greatereq_int(x782, x251)=true∧(∀x794,x795,x796,x797,x798:greatereq_int(pos(x793), pos(x792))=true∧pos(x794)=pos(x793)∧pos(0)=pos(x792)∧greatereq_int(x795, x796)=true ⇒ COND_EVAL1(true, pos(x794), x796, neg(x797), x798)≥EVAL(pos(x794), minus_int(x796, x798), plus_int(neg(x797), x796), x798)) ⇒ COND_EVAL1(true, pos(x254), x251, neg(x252), x253)≥EVAL(pos(x254), minus_int(x251, x253), plus_int(neg(x252), x251), x253))
(236) (greatereq_int(neg(x800), neg(x799))=true∧pos(x254)=neg(s(x800))∧pos(0)=neg(s(x799))∧greatereq_int(x782, x251)=true∧(∀x801,x802,x803,x804,x805:greatereq_int(neg(x800), neg(x799))=true∧pos(x801)=neg(x800)∧pos(0)=neg(x799)∧greatereq_int(x802, x803)=true ⇒ COND_EVAL1(true, pos(x801), x803, neg(x804), x805)≥EVAL(pos(x801), minus_int(x803, x805), plus_int(neg(x804), x803), x805)) ⇒ COND_EVAL1(true, pos(x254), x251, neg(x252), x253)≥EVAL(pos(x254), minus_int(x251, x253), plus_int(neg(x252), x251), x253))
(237) (greatereq_int(x782, x251)=true ⇒ COND_EVAL1(true, pos(x254), x251, neg(x252), x253)≥EVAL(pos(x254), minus_int(x251, x253), plus_int(neg(x252), x251), x253))
(238) (true=true ⇒ COND_EVAL1(true, pos(x254), pos(0), neg(x252), x253)≥EVAL(pos(x254), minus_int(pos(0), x253), plus_int(neg(x252), pos(0)), x253))
(239) (true=true ⇒ COND_EVAL1(true, pos(x254), pos(0), neg(x252), x253)≥EVAL(pos(x254), minus_int(pos(0), x253), plus_int(neg(x252), pos(0)), x253))
(240) (true=true ⇒ COND_EVAL1(true, pos(x254), neg(x808), neg(x252), x253)≥EVAL(pos(x254), minus_int(neg(x808), x253), plus_int(neg(x252), neg(x808)), x253))
(241) (true=true ⇒ COND_EVAL1(true, pos(x254), neg(x809), neg(x252), x253)≥EVAL(pos(x254), minus_int(neg(x809), x253), plus_int(neg(x252), neg(x809)), x253))
(242) (greatereq_int(pos(x816), pos(x815))=true∧(∀x817,x818,x819:greatereq_int(pos(x816), pos(x815))=true ⇒ COND_EVAL1(true, pos(x817), pos(x815), neg(x818), x819)≥EVAL(pos(x817), minus_int(pos(x815), x819), plus_int(neg(x818), pos(x815)), x819)) ⇒ COND_EVAL1(true, pos(x254), pos(s(x815)), neg(x252), x253)≥EVAL(pos(x254), minus_int(pos(s(x815)), x253), plus_int(neg(x252), pos(s(x815))), x253))
(243) (greatereq_int(neg(x821), neg(x820))=true∧(∀x822,x823,x824:greatereq_int(neg(x821), neg(x820))=true ⇒ COND_EVAL1(true, pos(x822), neg(x820), neg(x823), x824)≥EVAL(pos(x822), minus_int(neg(x820), x824), plus_int(neg(x823), neg(x820)), x824)) ⇒ COND_EVAL1(true, pos(x254), neg(s(x820)), neg(x252), x253)≥EVAL(pos(x254), minus_int(neg(s(x820)), x253), plus_int(neg(x252), neg(s(x820))), x253))
(244) (COND_EVAL1(true, pos(x254), pos(0), neg(x252), x253)≥EVAL(pos(x254), minus_int(pos(0), x253), plus_int(neg(x252), pos(0)), x253))
(245) (COND_EVAL1(true, pos(x254), pos(0), neg(x252), x253)≥EVAL(pos(x254), minus_int(pos(0), x253), plus_int(neg(x252), pos(0)), x253))
(246) (COND_EVAL1(true, pos(x254), neg(x808), neg(x252), x253)≥EVAL(pos(x254), minus_int(neg(x808), x253), plus_int(neg(x252), neg(x808)), x253))
(247) (COND_EVAL1(true, pos(x254), neg(x809), neg(x252), x253)≥EVAL(pos(x254), minus_int(neg(x809), x253), plus_int(neg(x252), neg(x809)), x253))
(248) (COND_EVAL1(true, pos(x254), pos(x815), neg(x252), x253)≥EVAL(pos(x254), minus_int(pos(x815), x253), plus_int(neg(x252), pos(x815)), x253) ⇒ COND_EVAL1(true, pos(x254), pos(s(x815)), neg(x252), x253)≥EVAL(pos(x254), minus_int(pos(s(x815)), x253), plus_int(neg(x252), pos(s(x815))), x253))
(249) (COND_EVAL1(true, pos(x254), neg(x820), neg(x252), x253)≥EVAL(pos(x254), minus_int(neg(x820), x253), plus_int(neg(x252), neg(x820)), x253) ⇒ COND_EVAL1(true, pos(x254), neg(s(x820)), neg(x252), x253)≥EVAL(pos(x254), minus_int(neg(s(x820)), x253), plus_int(neg(x252), neg(s(x820))), x253))
(250) (COND_EVAL1(and(greatereq_int(x262, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x264, x264), x264)), x263)), x262, x263, pos(x264), x265)=COND_EVAL1(true, pos(x266), x267, x268, x269) ⇒ COND_EVAL1(true, pos(x266), x267, x268, x269)≥EVAL(pos(x266), minus_int(x267, x269), plus_int(x268, x267), x269))
(251) (pos(x266)=x827∧pos(0)=x828∧greatereq_int(x827, x828)=x825∧greatereq_int(x829, x263)=x826∧and(x825, x826)=true ⇒ COND_EVAL1(true, pos(x266), x263, pos(x264), x265)≥EVAL(pos(x266), minus_int(x263, x265), plus_int(pos(x264), x263), x265))
(252) (true=true∧pos(x266)=x827∧pos(0)=x828∧greatereq_int(x827, x828)=true∧greatereq_int(x829, x263)=true ⇒ COND_EVAL1(true, pos(x266), x263, pos(x264), x265)≥EVAL(pos(x266), minus_int(x263, x265), plus_int(pos(x264), x263), x265))
(253) (pos(x266)=x827∧pos(0)=x828∧greatereq_int(x827, x828)=true∧greatereq_int(x829, x263)=true ⇒ COND_EVAL1(true, pos(x266), x263, pos(x264), x265)≥EVAL(pos(x266), minus_int(x263, x265), plus_int(pos(x264), x263), x265))
(254) (true=true∧pos(x266)=pos(x830)∧pos(0)=pos(0)∧greatereq_int(x829, x263)=true ⇒ COND_EVAL1(true, pos(x266), x263, pos(x264), x265)≥EVAL(pos(x266), minus_int(x263, x265), plus_int(pos(x264), x263), x265))
(255) (true=true∧pos(x266)=neg(0)∧pos(0)=pos(0)∧greatereq_int(x829, x263)=true ⇒ COND_EVAL1(true, pos(x266), x263, pos(x264), x265)≥EVAL(pos(x266), minus_int(x263, x265), plus_int(pos(x264), x263), x265))
(256) (true=true∧pos(x266)=neg(0)∧pos(0)=neg(x832)∧greatereq_int(x829, x263)=true ⇒ COND_EVAL1(true, pos(x266), x263, pos(x264), x265)≥EVAL(pos(x266), minus_int(x263, x265), plus_int(pos(x264), x263), x265))
(257) (true=true∧pos(x266)=pos(x834)∧pos(0)=neg(x833)∧greatereq_int(x829, x263)=true ⇒ COND_EVAL1(true, pos(x266), x263, pos(x264), x265)≥EVAL(pos(x266), minus_int(x263, x265), plus_int(pos(x264), x263), x265))
(258) (greatereq_int(pos(x840), pos(x839))=true∧pos(x266)=pos(s(x840))∧pos(0)=pos(s(x839))∧greatereq_int(x829, x263)=true∧(∀x841,x842,x843,x844,x845:greatereq_int(pos(x840), pos(x839))=true∧pos(x841)=pos(x840)∧pos(0)=pos(x839)∧greatereq_int(x842, x843)=true ⇒ COND_EVAL1(true, pos(x841), x843, pos(x844), x845)≥EVAL(pos(x841), minus_int(x843, x845), plus_int(pos(x844), x843), x845)) ⇒ COND_EVAL1(true, pos(x266), x263, pos(x264), x265)≥EVAL(pos(x266), minus_int(x263, x265), plus_int(pos(x264), x263), x265))
(259) (greatereq_int(neg(x847), neg(x846))=true∧pos(x266)=neg(s(x847))∧pos(0)=neg(s(x846))∧greatereq_int(x829, x263)=true∧(∀x848,x849,x850,x851,x852:greatereq_int(neg(x847), neg(x846))=true∧pos(x848)=neg(x847)∧pos(0)=neg(x846)∧greatereq_int(x849, x850)=true ⇒ COND_EVAL1(true, pos(x848), x850, pos(x851), x852)≥EVAL(pos(x848), minus_int(x850, x852), plus_int(pos(x851), x850), x852)) ⇒ COND_EVAL1(true, pos(x266), x263, pos(x264), x265)≥EVAL(pos(x266), minus_int(x263, x265), plus_int(pos(x264), x263), x265))
(260) (greatereq_int(x829, x263)=true ⇒ COND_EVAL1(true, pos(x266), x263, pos(x264), x265)≥EVAL(pos(x266), minus_int(x263, x265), plus_int(pos(x264), x263), x265))
(261) (true=true ⇒ COND_EVAL1(true, pos(x266), pos(0), pos(x264), x265)≥EVAL(pos(x266), minus_int(pos(0), x265), plus_int(pos(x264), pos(0)), x265))
(262) (true=true ⇒ COND_EVAL1(true, pos(x266), pos(0), pos(x264), x265)≥EVAL(pos(x266), minus_int(pos(0), x265), plus_int(pos(x264), pos(0)), x265))
(263) (true=true ⇒ COND_EVAL1(true, pos(x266), neg(x855), pos(x264), x265)≥EVAL(pos(x266), minus_int(neg(x855), x265), plus_int(pos(x264), neg(x855)), x265))
(264) (true=true ⇒ COND_EVAL1(true, pos(x266), neg(x856), pos(x264), x265)≥EVAL(pos(x266), minus_int(neg(x856), x265), plus_int(pos(x264), neg(x856)), x265))
(265) (greatereq_int(pos(x863), pos(x862))=true∧(∀x864,x865,x866:greatereq_int(pos(x863), pos(x862))=true ⇒ COND_EVAL1(true, pos(x864), pos(x862), pos(x865), x866)≥EVAL(pos(x864), minus_int(pos(x862), x866), plus_int(pos(x865), pos(x862)), x866)) ⇒ COND_EVAL1(true, pos(x266), pos(s(x862)), pos(x264), x265)≥EVAL(pos(x266), minus_int(pos(s(x862)), x265), plus_int(pos(x264), pos(s(x862))), x265))
(266) (greatereq_int(neg(x868), neg(x867))=true∧(∀x869,x870,x871:greatereq_int(neg(x868), neg(x867))=true ⇒ COND_EVAL1(true, pos(x869), neg(x867), pos(x870), x871)≥EVAL(pos(x869), minus_int(neg(x867), x871), plus_int(pos(x870), neg(x867)), x871)) ⇒ COND_EVAL1(true, pos(x266), neg(s(x867)), pos(x264), x265)≥EVAL(pos(x266), minus_int(neg(s(x867)), x265), plus_int(pos(x264), neg(s(x867))), x265))
(267) (COND_EVAL1(true, pos(x266), pos(0), pos(x264), x265)≥EVAL(pos(x266), minus_int(pos(0), x265), plus_int(pos(x264), pos(0)), x265))
(268) (COND_EVAL1(true, pos(x266), pos(0), pos(x264), x265)≥EVAL(pos(x266), minus_int(pos(0), x265), plus_int(pos(x264), pos(0)), x265))
(269) (COND_EVAL1(true, pos(x266), neg(x855), pos(x264), x265)≥EVAL(pos(x266), minus_int(neg(x855), x265), plus_int(pos(x264), neg(x855)), x265))
(270) (COND_EVAL1(true, pos(x266), neg(x856), pos(x264), x265)≥EVAL(pos(x266), minus_int(neg(x856), x265), plus_int(pos(x264), neg(x856)), x265))
(271) (COND_EVAL1(true, pos(x266), pos(x862), pos(x264), x265)≥EVAL(pos(x266), minus_int(pos(x862), x265), plus_int(pos(x264), pos(x862)), x265) ⇒ COND_EVAL1(true, pos(x266), pos(s(x862)), pos(x264), x265)≥EVAL(pos(x266), minus_int(pos(s(x862)), x265), plus_int(pos(x264), pos(s(x862))), x265))
(272) (COND_EVAL1(true, pos(x266), neg(x867), pos(x264), x265)≥EVAL(pos(x266), minus_int(neg(x867), x265), plus_int(pos(x264), neg(x867)), x265) ⇒ COND_EVAL1(true, pos(x266), neg(s(x867)), pos(x264), x265)≥EVAL(pos(x266), minus_int(neg(s(x867)), x265), plus_int(pos(x264), neg(s(x867))), x265))
(273) (EVAL(x273, minus_int(x274, x276), plus_int(pos(x275), x274), x276)=EVAL(x277, x278, neg(x279), x280) ⇒ EVAL(x277, x278, neg(x279), x280)≥COND_EVAL1(and(greatereq_int(x277, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x279, x279), x279)), x278)), x277, x278, neg(x279), x280))
(274) (minus_int(x274, x276)=x278∧pos(x275)=x872∧plus_int(x872, x274)=neg(x279) ⇒ EVAL(x273, x278, neg(x279), x276)≥COND_EVAL1(and(greatereq_int(x273, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x279, x279), x279)), x278)), x273, x278, neg(x279), x276))
(275) (minus_nat(x874, x873)=neg(x279)∧minus_int(neg(x873), x276)=x278∧pos(x275)=pos(x874) ⇒ EVAL(x273, x278, neg(x279), x276)≥COND_EVAL1(and(greatereq_int(x273, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x279, x279), x279)), x278)), x273, x278, neg(x279), x276))
(276) (minus_nat(x875, x876)=neg(x279)∧minus_int(pos(x875), x276)=x278∧pos(x275)=neg(x876) ⇒ EVAL(x273, x278, neg(x279), x276)≥COND_EVAL1(and(greatereq_int(x273, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x279, x279), x279)), x278)), x273, x278, neg(x279), x276))
(277) (neg(plus_nat(x878, x877))=neg(x279)∧minus_int(neg(x877), x276)=x278∧pos(x275)=neg(x878) ⇒ EVAL(x273, x278, neg(x279), x276)≥COND_EVAL1(and(greatereq_int(x273, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x279, x279), x279)), x278)), x273, x278, neg(x279), x276))
(278) (minus_nat(x874, x873)=neg(x279)∧neg(x873)=x881∧minus_int(x881, x276)=x278 ⇒ EVAL(x273, x278, neg(x279), x276)≥COND_EVAL1(and(greatereq_int(x273, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x279, x279), x279)), x278)), x273, x278, neg(x279), x276))
(279) (neg(s(x882))=neg(x279)∧neg(s(x882))=x881∧minus_int(x881, x276)=x278 ⇒ EVAL(x273, x278, neg(x279), x276)≥COND_EVAL1(and(greatereq_int(x273, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x279, x279), x279)), x278)), x273, x278, neg(x279), x276))
(280) (minus_nat(x885, x884)=neg(x279)∧neg(s(x884))=x881∧minus_int(x881, x276)=x278∧(∀x886,x887,x888,x889,x890:minus_nat(x885, x884)=neg(x886)∧neg(x884)=x887∧minus_int(x887, x888)=x889 ⇒ EVAL(x890, x889, neg(x886), x888)≥COND_EVAL1(and(greatereq_int(x890, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x886, x886), x886)), x889)), x890, x889, neg(x886), x888)) ⇒ EVAL(x273, x278, neg(x279), x276)≥COND_EVAL1(and(greatereq_int(x273, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x279, x279), x279)), x278)), x273, x278, neg(x279), x276))
(281) (EVAL(x273, x278, neg(s(x882)), x276)≥COND_EVAL1(and(greatereq_int(x273, pos(0)), greatereq_int(neg(mult_nat(mult_nat(s(x882), s(x882)), s(x882))), x278)), x273, x278, neg(s(x882)), x276))
(282) (EVAL(x273, x278, neg(x279), x276)≥COND_EVAL1(and(greatereq_int(x273, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x279, x279), x279)), x278)), x273, x278, neg(x279), x276))
(283) (EVAL(x281, minus_int(x282, x284), plus_int(neg(x283), x282), x284)=EVAL(x285, x286, neg(x287), x288) ⇒ EVAL(x285, x286, neg(x287), x288)≥COND_EVAL1(and(greatereq_int(x285, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x287, x287), x287)), x286)), x285, x286, neg(x287), x288))
(284) (minus_int(x282, x284)=x286∧neg(x283)=x891∧plus_int(x891, x282)=neg(x287) ⇒ EVAL(x281, x286, neg(x287), x284)≥COND_EVAL1(and(greatereq_int(x281, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x287, x287), x287)), x286)), x281, x286, neg(x287), x284))
(285) (minus_nat(x893, x892)=neg(x287)∧minus_int(neg(x892), x284)=x286∧neg(x283)=pos(x893) ⇒ EVAL(x281, x286, neg(x287), x284)≥COND_EVAL1(and(greatereq_int(x281, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x287, x287), x287)), x286)), x281, x286, neg(x287), x284))
(286) (minus_nat(x894, x895)=neg(x287)∧minus_int(pos(x894), x284)=x286∧neg(x283)=neg(x895) ⇒ EVAL(x281, x286, neg(x287), x284)≥COND_EVAL1(and(greatereq_int(x281, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x287, x287), x287)), x286)), x281, x286, neg(x287), x284))
(287) (neg(plus_nat(x897, x896))=neg(x287)∧minus_int(neg(x896), x284)=x286∧neg(x283)=neg(x897) ⇒ EVAL(x281, x286, neg(x287), x284)≥COND_EVAL1(and(greatereq_int(x281, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x287, x287), x287)), x286)), x281, x286, neg(x287), x284))
(288) (minus_nat(x894, x895)=neg(x287)∧pos(x894)=x900∧minus_int(x900, x284)=x286 ⇒ EVAL(x281, x286, neg(x287), x284)≥COND_EVAL1(and(greatereq_int(x281, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x287, x287), x287)), x286)), x281, x286, neg(x287), x284))
(289) (neg(s(x901))=neg(x287)∧pos(0)=x900∧minus_int(x900, x284)=x286 ⇒ EVAL(x281, x286, neg(x287), x284)≥COND_EVAL1(and(greatereq_int(x281, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x287, x287), x287)), x286)), x281, x286, neg(x287), x284))
(290) (minus_nat(x904, x903)=neg(x287)∧pos(s(x904))=x900∧minus_int(x900, x284)=x286∧(∀x905,x906,x907,x908,x909:minus_nat(x904, x903)=neg(x905)∧pos(x904)=x906∧minus_int(x906, x907)=x908 ⇒ EVAL(x909, x908, neg(x905), x907)≥COND_EVAL1(and(greatereq_int(x909, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x905, x905), x905)), x908)), x909, x908, neg(x905), x907)) ⇒ EVAL(x281, x286, neg(x287), x284)≥COND_EVAL1(and(greatereq_int(x281, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x287, x287), x287)), x286)), x281, x286, neg(x287), x284))
(291) (EVAL(x281, x286, neg(s(x901)), x284)≥COND_EVAL1(and(greatereq_int(x281, pos(0)), greatereq_int(neg(mult_nat(mult_nat(s(x901), s(x901)), s(x901))), x286)), x281, x286, neg(s(x901)), x284))
(292) (EVAL(x281, x286, neg(x287), x284)≥COND_EVAL1(and(greatereq_int(x281, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x287, x287), x287)), x286)), x281, x286, neg(x287), x284))
(293) (EVAL(neg(0), minus_int(x289, x291), plus_int(x290, x289), x291)=EVAL(x292, x293, neg(x294), x295) ⇒ EVAL(x292, x293, neg(x294), x295)≥COND_EVAL1(and(greatereq_int(x292, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x294, x294), x294)), x293)), x292, x293, neg(x294), x295))
(294) (minus_int(x289, x291)=x293∧plus_int(x290, x289)=neg(x294) ⇒ EVAL(neg(0), x293, neg(x294), x291)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x294, x294), x294)), x293)), neg(0), x293, neg(x294), x291))
(295) (minus_nat(x912, x911)=neg(x294)∧minus_int(neg(x911), x291)=x293 ⇒ EVAL(neg(0), x293, neg(x294), x291)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x294, x294), x294)), x293)), neg(0), x293, neg(x294), x291))
(296) (minus_nat(x913, x914)=neg(x294)∧minus_int(pos(x913), x291)=x293 ⇒ EVAL(neg(0), x293, neg(x294), x291)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x294, x294), x294)), x293)), neg(0), x293, neg(x294), x291))
(297) (neg(plus_nat(x916, x915))=neg(x294)∧minus_int(neg(x915), x291)=x293 ⇒ EVAL(neg(0), x293, neg(x294), x291)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x294, x294), x294)), x293)), neg(0), x293, neg(x294), x291))
(298) (minus_nat(x912, x911)=neg(x294)∧neg(x911)=x919∧minus_int(x919, x291)=x293 ⇒ EVAL(neg(0), x293, neg(x294), x291)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x294, x294), x294)), x293)), neg(0), x293, neg(x294), x291))
(299) (minus_nat(x913, x914)=neg(x294)∧pos(x913)=x928∧minus_int(x928, x291)=x293 ⇒ EVAL(neg(0), x293, neg(x294), x291)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x294, x294), x294)), x293)), neg(0), x293, neg(x294), x291))
(300) (neg(s(x920))=neg(x294)∧neg(s(x920))=x919∧minus_int(x919, x291)=x293 ⇒ EVAL(neg(0), x293, neg(x294), x291)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x294, x294), x294)), x293)), neg(0), x293, neg(x294), x291))
(301) (minus_nat(x923, x922)=neg(x294)∧neg(s(x922))=x919∧minus_int(x919, x291)=x293∧(∀x924,x925,x926,x927:minus_nat(x923, x922)=neg(x924)∧neg(x922)=x925∧minus_int(x925, x926)=x927 ⇒ EVAL(neg(0), x927, neg(x924), x926)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x924, x924), x924)), x927)), neg(0), x927, neg(x924), x926)) ⇒ EVAL(neg(0), x293, neg(x294), x291)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x294, x294), x294)), x293)), neg(0), x293, neg(x294), x291))
(302) (EVAL(neg(0), x293, neg(s(x920)), x291)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(neg(mult_nat(mult_nat(s(x920), s(x920)), s(x920))), x293)), neg(0), x293, neg(s(x920)), x291))
(303) (EVAL(neg(0), x293, neg(x294), x291)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x294, x294), x294)), x293)), neg(0), x293, neg(x294), x291))
(304) (neg(s(x929))=neg(x294)∧pos(0)=x928∧minus_int(x928, x291)=x293 ⇒ EVAL(neg(0), x293, neg(x294), x291)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x294, x294), x294)), x293)), neg(0), x293, neg(x294), x291))
(305) (minus_nat(x932, x931)=neg(x294)∧pos(s(x932))=x928∧minus_int(x928, x291)=x293∧(∀x933,x934,x935,x936:minus_nat(x932, x931)=neg(x933)∧pos(x932)=x934∧minus_int(x934, x935)=x936 ⇒ EVAL(neg(0), x936, neg(x933), x935)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x933, x933), x933)), x936)), neg(0), x936, neg(x933), x935)) ⇒ EVAL(neg(0), x293, neg(x294), x291)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x294, x294), x294)), x293)), neg(0), x293, neg(x294), x291))
(306) (EVAL(neg(0), x293, neg(s(x929)), x291)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(neg(mult_nat(mult_nat(s(x929), s(x929)), s(x929))), x293)), neg(0), x293, neg(s(x929)), x291))
(307) (EVAL(neg(0), x293, neg(x294), x291)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x294, x294), x294)), x293)), neg(0), x293, neg(x294), x291))
(308) (EVAL(pos(x300), minus_int(x301, x303), plus_int(x302, x301), x303)=EVAL(x304, x305, neg(x306), x307) ⇒ EVAL(x304, x305, neg(x306), x307)≥COND_EVAL1(and(greatereq_int(x304, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x306, x306), x306)), x305)), x304, x305, neg(x306), x307))
(309) (minus_int(x301, x303)=x305∧plus_int(x302, x301)=neg(x306) ⇒ EVAL(pos(x300), x305, neg(x306), x303)≥COND_EVAL1(and(greatereq_int(pos(x300), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x306, x306), x306)), x305)), pos(x300), x305, neg(x306), x303))
(310) (minus_nat(x939, x938)=neg(x306)∧minus_int(neg(x938), x303)=x305 ⇒ EVAL(pos(x300), x305, neg(x306), x303)≥COND_EVAL1(and(greatereq_int(pos(x300), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x306, x306), x306)), x305)), pos(x300), x305, neg(x306), x303))
(311) (minus_nat(x940, x941)=neg(x306)∧minus_int(pos(x940), x303)=x305 ⇒ EVAL(pos(x300), x305, neg(x306), x303)≥COND_EVAL1(and(greatereq_int(pos(x300), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x306, x306), x306)), x305)), pos(x300), x305, neg(x306), x303))
(312) (neg(plus_nat(x943, x942))=neg(x306)∧minus_int(neg(x942), x303)=x305 ⇒ EVAL(pos(x300), x305, neg(x306), x303)≥COND_EVAL1(and(greatereq_int(pos(x300), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x306, x306), x306)), x305)), pos(x300), x305, neg(x306), x303))
(313) (minus_nat(x939, x938)=neg(x306)∧neg(x938)=x946∧minus_int(x946, x303)=x305 ⇒ EVAL(pos(x300), x305, neg(x306), x303)≥COND_EVAL1(and(greatereq_int(pos(x300), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x306, x306), x306)), x305)), pos(x300), x305, neg(x306), x303))
(314) (minus_nat(x940, x941)=neg(x306)∧pos(x940)=x956∧minus_int(x956, x303)=x305 ⇒ EVAL(pos(x300), x305, neg(x306), x303)≥COND_EVAL1(and(greatereq_int(pos(x300), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x306, x306), x306)), x305)), pos(x300), x305, neg(x306), x303))
(315) (neg(s(x947))=neg(x306)∧neg(s(x947))=x946∧minus_int(x946, x303)=x305 ⇒ EVAL(pos(x300), x305, neg(x306), x303)≥COND_EVAL1(and(greatereq_int(pos(x300), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x306, x306), x306)), x305)), pos(x300), x305, neg(x306), x303))
(316) (minus_nat(x950, x949)=neg(x306)∧neg(s(x949))=x946∧minus_int(x946, x303)=x305∧(∀x951,x952,x953,x954,x955:minus_nat(x950, x949)=neg(x951)∧neg(x949)=x952∧minus_int(x952, x953)=x954 ⇒ EVAL(pos(x955), x954, neg(x951), x953)≥COND_EVAL1(and(greatereq_int(pos(x955), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x951, x951), x951)), x954)), pos(x955), x954, neg(x951), x953)) ⇒ EVAL(pos(x300), x305, neg(x306), x303)≥COND_EVAL1(and(greatereq_int(pos(x300), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x306, x306), x306)), x305)), pos(x300), x305, neg(x306), x303))
(317) (EVAL(pos(x300), x305, neg(s(x947)), x303)≥COND_EVAL1(and(greatereq_int(pos(x300), pos(0)), greatereq_int(neg(mult_nat(mult_nat(s(x947), s(x947)), s(x947))), x305)), pos(x300), x305, neg(s(x947)), x303))
(318) (EVAL(pos(x300), x305, neg(x306), x303)≥COND_EVAL1(and(greatereq_int(pos(x300), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x306, x306), x306)), x305)), pos(x300), x305, neg(x306), x303))
(319) (neg(s(x957))=neg(x306)∧pos(0)=x956∧minus_int(x956, x303)=x305 ⇒ EVAL(pos(x300), x305, neg(x306), x303)≥COND_EVAL1(and(greatereq_int(pos(x300), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x306, x306), x306)), x305)), pos(x300), x305, neg(x306), x303))
(320) (minus_nat(x960, x959)=neg(x306)∧pos(s(x960))=x956∧minus_int(x956, x303)=x305∧(∀x961,x962,x963,x964,x965:minus_nat(x960, x959)=neg(x961)∧pos(x960)=x962∧minus_int(x962, x963)=x964 ⇒ EVAL(pos(x965), x964, neg(x961), x963)≥COND_EVAL1(and(greatereq_int(pos(x965), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x961, x961), x961)), x964)), pos(x965), x964, neg(x961), x963)) ⇒ EVAL(pos(x300), x305, neg(x306), x303)≥COND_EVAL1(and(greatereq_int(pos(x300), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x306, x306), x306)), x305)), pos(x300), x305, neg(x306), x303))
(321) (EVAL(pos(x300), x305, neg(s(x957)), x303)≥COND_EVAL1(and(greatereq_int(pos(x300), pos(0)), greatereq_int(neg(mult_nat(mult_nat(s(x957), s(x957)), s(x957))), x305)), pos(x300), x305, neg(s(x957)), x303))
(322) (EVAL(pos(x300), x305, neg(x306), x303)≥COND_EVAL1(and(greatereq_int(pos(x300), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x306, x306), x306)), x305)), pos(x300), x305, neg(x306), x303))
(323) (EVAL(neg(s(x312)), minus_int(x313, x315), plus_int(x314, x313), x315)=EVAL(x316, x317, neg(x318), x319) ⇒ EVAL(x316, x317, neg(x318), x319)≥COND_EVAL1(and(greatereq_int(x316, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x318, x318), x318)), x317)), x316, x317, neg(x318), x319))
(324) (minus_int(x313, x315)=x317∧plus_int(x314, x313)=neg(x318) ⇒ EVAL(neg(s(x312)), x317, neg(x318), x315)≥COND_EVAL1(and(greatereq_int(neg(s(x312)), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x318, x318), x318)), x317)), neg(s(x312)), x317, neg(x318), x315))
(325) (minus_nat(x968, x967)=neg(x318)∧minus_int(neg(x967), x315)=x317 ⇒ EVAL(neg(s(x312)), x317, neg(x318), x315)≥COND_EVAL1(and(greatereq_int(neg(s(x312)), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x318, x318), x318)), x317)), neg(s(x312)), x317, neg(x318), x315))
(326) (minus_nat(x969, x970)=neg(x318)∧minus_int(pos(x969), x315)=x317 ⇒ EVAL(neg(s(x312)), x317, neg(x318), x315)≥COND_EVAL1(and(greatereq_int(neg(s(x312)), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x318, x318), x318)), x317)), neg(s(x312)), x317, neg(x318), x315))
(327) (neg(plus_nat(x972, x971))=neg(x318)∧minus_int(neg(x971), x315)=x317 ⇒ EVAL(neg(s(x312)), x317, neg(x318), x315)≥COND_EVAL1(and(greatereq_int(neg(s(x312)), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x318, x318), x318)), x317)), neg(s(x312)), x317, neg(x318), x315))
(328) (minus_nat(x968, x967)=neg(x318)∧neg(x967)=x975∧minus_int(x975, x315)=x317 ⇒ EVAL(neg(s(x312)), x317, neg(x318), x315)≥COND_EVAL1(and(greatereq_int(neg(s(x312)), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x318, x318), x318)), x317)), neg(s(x312)), x317, neg(x318), x315))
(329) (minus_nat(x969, x970)=neg(x318)∧pos(x969)=x985∧minus_int(x985, x315)=x317 ⇒ EVAL(neg(s(x312)), x317, neg(x318), x315)≥COND_EVAL1(and(greatereq_int(neg(s(x312)), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x318, x318), x318)), x317)), neg(s(x312)), x317, neg(x318), x315))
(330) (neg(s(x976))=neg(x318)∧neg(s(x976))=x975∧minus_int(x975, x315)=x317 ⇒ EVAL(neg(s(x312)), x317, neg(x318), x315)≥COND_EVAL1(and(greatereq_int(neg(s(x312)), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x318, x318), x318)), x317)), neg(s(x312)), x317, neg(x318), x315))
(331) (minus_nat(x979, x978)=neg(x318)∧neg(s(x978))=x975∧minus_int(x975, x315)=x317∧(∀x980,x981,x982,x983,x984:minus_nat(x979, x978)=neg(x980)∧neg(x978)=x981∧minus_int(x981, x982)=x983 ⇒ EVAL(neg(s(x984)), x983, neg(x980), x982)≥COND_EVAL1(and(greatereq_int(neg(s(x984)), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x980, x980), x980)), x983)), neg(s(x984)), x983, neg(x980), x982)) ⇒ EVAL(neg(s(x312)), x317, neg(x318), x315)≥COND_EVAL1(and(greatereq_int(neg(s(x312)), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x318, x318), x318)), x317)), neg(s(x312)), x317, neg(x318), x315))
(332) (EVAL(neg(s(x312)), x317, neg(s(x976)), x315)≥COND_EVAL1(and(greatereq_int(neg(s(x312)), pos(0)), greatereq_int(neg(mult_nat(mult_nat(s(x976), s(x976)), s(x976))), x317)), neg(s(x312)), x317, neg(s(x976)), x315))
(333) (EVAL(neg(s(x312)), x317, neg(x318), x315)≥COND_EVAL1(and(greatereq_int(neg(s(x312)), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x318, x318), x318)), x317)), neg(s(x312)), x317, neg(x318), x315))
(334) (neg(s(x986))=neg(x318)∧pos(0)=x985∧minus_int(x985, x315)=x317 ⇒ EVAL(neg(s(x312)), x317, neg(x318), x315)≥COND_EVAL1(and(greatereq_int(neg(s(x312)), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x318, x318), x318)), x317)), neg(s(x312)), x317, neg(x318), x315))
(335) (minus_nat(x989, x988)=neg(x318)∧pos(s(x989))=x985∧minus_int(x985, x315)=x317∧(∀x990,x991,x992,x993,x994:minus_nat(x989, x988)=neg(x990)∧pos(x989)=x991∧minus_int(x991, x992)=x993 ⇒ EVAL(neg(s(x994)), x993, neg(x990), x992)≥COND_EVAL1(and(greatereq_int(neg(s(x994)), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x990, x990), x990)), x993)), neg(s(x994)), x993, neg(x990), x992)) ⇒ EVAL(neg(s(x312)), x317, neg(x318), x315)≥COND_EVAL1(and(greatereq_int(neg(s(x312)), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x318, x318), x318)), x317)), neg(s(x312)), x317, neg(x318), x315))
(336) (EVAL(neg(s(x312)), x317, neg(s(x986)), x315)≥COND_EVAL1(and(greatereq_int(neg(s(x312)), pos(0)), greatereq_int(neg(mult_nat(mult_nat(s(x986), s(x986)), s(x986))), x317)), neg(s(x312)), x317, neg(s(x986)), x315))
(337) (EVAL(neg(s(x312)), x317, neg(x318), x315)≥COND_EVAL1(and(greatereq_int(neg(s(x312)), pos(0)), greatereq_int(neg(mult_nat(mult_nat(x318, x318), x318)), x317)), neg(s(x312)), x317, neg(x318), x315))
(338) (COND_EVAL1(and(greatereq_int(x346, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x348, x348), x348)), x347)), x346, x347, neg(x348), x349)=COND_EVAL1(true, neg(s(x350)), x351, x352, x353) ⇒ COND_EVAL1(true, neg(s(x350)), x351, x352, x353)≥EVAL(neg(s(x350)), minus_int(x351, x353), plus_int(x352, x351), x353))
(339) (neg(s(x350))=x998∧pos(0)=x999∧greatereq_int(x998, x999)=x996∧greatereq_int(x1000, x347)=x997∧and(x996, x997)=true ⇒ COND_EVAL1(true, neg(s(x350)), x347, neg(x348), x349)≥EVAL(neg(s(x350)), minus_int(x347, x349), plus_int(neg(x348), x347), x349))
(340) (true=true∧neg(s(x350))=x998∧pos(0)=x999∧greatereq_int(x998, x999)=true∧greatereq_int(x1000, x347)=true ⇒ COND_EVAL1(true, neg(s(x350)), x347, neg(x348), x349)≥EVAL(neg(s(x350)), minus_int(x347, x349), plus_int(neg(x348), x347), x349))
(341) (neg(s(x350))=x998∧pos(0)=x999∧greatereq_int(x998, x999)=true∧greatereq_int(x1000, x347)=true ⇒ COND_EVAL1(true, neg(s(x350)), x347, neg(x348), x349)≥EVAL(neg(s(x350)), minus_int(x347, x349), plus_int(neg(x348), x347), x349))
(342) (true=true∧neg(s(x350))=pos(x1001)∧pos(0)=pos(0)∧greatereq_int(x1000, x347)=true ⇒ COND_EVAL1(true, neg(s(x350)), x347, neg(x348), x349)≥EVAL(neg(s(x350)), minus_int(x347, x349), plus_int(neg(x348), x347), x349))
(343) (true=true∧neg(s(x350))=neg(0)∧pos(0)=pos(0)∧greatereq_int(x1000, x347)=true ⇒ COND_EVAL1(true, neg(s(x350)), x347, neg(x348), x349)≥EVAL(neg(s(x350)), minus_int(x347, x349), plus_int(neg(x348), x347), x349))
(344) (true=true∧neg(s(x350))=neg(0)∧pos(0)=neg(x1003)∧greatereq_int(x1000, x347)=true ⇒ COND_EVAL1(true, neg(s(x350)), x347, neg(x348), x349)≥EVAL(neg(s(x350)), minus_int(x347, x349), plus_int(neg(x348), x347), x349))
(345) (true=true∧neg(s(x350))=pos(x1005)∧pos(0)=neg(x1004)∧greatereq_int(x1000, x347)=true ⇒ COND_EVAL1(true, neg(s(x350)), x347, neg(x348), x349)≥EVAL(neg(s(x350)), minus_int(x347, x349), plus_int(neg(x348), x347), x349))
(346) (greatereq_int(pos(x1011), pos(x1010))=true∧neg(s(x350))=pos(s(x1011))∧pos(0)=pos(s(x1010))∧greatereq_int(x1000, x347)=true∧(∀x1012,x1013,x1014,x1015,x1016:greatereq_int(pos(x1011), pos(x1010))=true∧neg(s(x1012))=pos(x1011)∧pos(0)=pos(x1010)∧greatereq_int(x1013, x1014)=true ⇒ COND_EVAL1(true, neg(s(x1012)), x1014, neg(x1015), x1016)≥EVAL(neg(s(x1012)), minus_int(x1014, x1016), plus_int(neg(x1015), x1014), x1016)) ⇒ COND_EVAL1(true, neg(s(x350)), x347, neg(x348), x349)≥EVAL(neg(s(x350)), minus_int(x347, x349), plus_int(neg(x348), x347), x349))
(347) (greatereq_int(neg(x1018), neg(x1017))=true∧neg(s(x350))=neg(s(x1018))∧pos(0)=neg(s(x1017))∧greatereq_int(x1000, x347)=true∧(∀x1019,x1020,x1021,x1022,x1023:greatereq_int(neg(x1018), neg(x1017))=true∧neg(s(x1019))=neg(x1018)∧pos(0)=neg(x1017)∧greatereq_int(x1020, x1021)=true ⇒ COND_EVAL1(true, neg(s(x1019)), x1021, neg(x1022), x1023)≥EVAL(neg(s(x1019)), minus_int(x1021, x1023), plus_int(neg(x1022), x1021), x1023)) ⇒ COND_EVAL1(true, neg(s(x350)), x347, neg(x348), x349)≥EVAL(neg(s(x350)), minus_int(x347, x349), plus_int(neg(x348), x347), x349))
(348) (COND_EVAL1(and(greatereq_int(x358, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x360, x360), x360)), x359)), x358, x359, pos(x360), x361)=COND_EVAL1(true, neg(s(x362)), x363, x364, x365) ⇒ COND_EVAL1(true, neg(s(x362)), x363, x364, x365)≥EVAL(neg(s(x362)), minus_int(x363, x365), plus_int(x364, x363), x365))
(349) (neg(s(x362))=x1026∧pos(0)=x1027∧greatereq_int(x1026, x1027)=x1024∧greatereq_int(x1028, x359)=x1025∧and(x1024, x1025)=true ⇒ COND_EVAL1(true, neg(s(x362)), x359, pos(x360), x361)≥EVAL(neg(s(x362)), minus_int(x359, x361), plus_int(pos(x360), x359), x361))
(350) (true=true∧neg(s(x362))=x1026∧pos(0)=x1027∧greatereq_int(x1026, x1027)=true∧greatereq_int(x1028, x359)=true ⇒ COND_EVAL1(true, neg(s(x362)), x359, pos(x360), x361)≥EVAL(neg(s(x362)), minus_int(x359, x361), plus_int(pos(x360), x359), x361))
(351) (neg(s(x362))=x1026∧pos(0)=x1027∧greatereq_int(x1026, x1027)=true∧greatereq_int(x1028, x359)=true ⇒ COND_EVAL1(true, neg(s(x362)), x359, pos(x360), x361)≥EVAL(neg(s(x362)), minus_int(x359, x361), plus_int(pos(x360), x359), x361))
(352) (true=true∧neg(s(x362))=pos(x1029)∧pos(0)=pos(0)∧greatereq_int(x1028, x359)=true ⇒ COND_EVAL1(true, neg(s(x362)), x359, pos(x360), x361)≥EVAL(neg(s(x362)), minus_int(x359, x361), plus_int(pos(x360), x359), x361))
(353) (true=true∧neg(s(x362))=neg(0)∧pos(0)=pos(0)∧greatereq_int(x1028, x359)=true ⇒ COND_EVAL1(true, neg(s(x362)), x359, pos(x360), x361)≥EVAL(neg(s(x362)), minus_int(x359, x361), plus_int(pos(x360), x359), x361))
(354) (true=true∧neg(s(x362))=neg(0)∧pos(0)=neg(x1031)∧greatereq_int(x1028, x359)=true ⇒ COND_EVAL1(true, neg(s(x362)), x359, pos(x360), x361)≥EVAL(neg(s(x362)), minus_int(x359, x361), plus_int(pos(x360), x359), x361))
(355) (true=true∧neg(s(x362))=pos(x1033)∧pos(0)=neg(x1032)∧greatereq_int(x1028, x359)=true ⇒ COND_EVAL1(true, neg(s(x362)), x359, pos(x360), x361)≥EVAL(neg(s(x362)), minus_int(x359, x361), plus_int(pos(x360), x359), x361))
(356) (greatereq_int(pos(x1039), pos(x1038))=true∧neg(s(x362))=pos(s(x1039))∧pos(0)=pos(s(x1038))∧greatereq_int(x1028, x359)=true∧(∀x1040,x1041,x1042,x1043,x1044:greatereq_int(pos(x1039), pos(x1038))=true∧neg(s(x1040))=pos(x1039)∧pos(0)=pos(x1038)∧greatereq_int(x1041, x1042)=true ⇒ COND_EVAL1(true, neg(s(x1040)), x1042, pos(x1043), x1044)≥EVAL(neg(s(x1040)), minus_int(x1042, x1044), plus_int(pos(x1043), x1042), x1044)) ⇒ COND_EVAL1(true, neg(s(x362)), x359, pos(x360), x361)≥EVAL(neg(s(x362)), minus_int(x359, x361), plus_int(pos(x360), x359), x361))
(357) (greatereq_int(neg(x1046), neg(x1045))=true∧neg(s(x362))=neg(s(x1046))∧pos(0)=neg(s(x1045))∧greatereq_int(x1028, x359)=true∧(∀x1047,x1048,x1049,x1050,x1051:greatereq_int(neg(x1046), neg(x1045))=true∧neg(s(x1047))=neg(x1046)∧pos(0)=neg(x1045)∧greatereq_int(x1048, x1049)=true ⇒ COND_EVAL1(true, neg(s(x1047)), x1049, pos(x1050), x1051)≥EVAL(neg(s(x1047)), minus_int(x1049, x1051), plus_int(pos(x1050), x1049), x1051)) ⇒ COND_EVAL1(true, neg(s(x362)), x359, pos(x360), x361)≥EVAL(neg(s(x362)), minus_int(x359, x361), plus_int(pos(x360), x359), x361))
(358) (EVAL(x369, minus_int(x370, x372), plus_int(pos(x371), x370), x372)=EVAL(x373, x374, pos(x375), x376) ⇒ EVAL(x373, x374, pos(x375), x376)≥COND_EVAL1(and(greatereq_int(x373, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x375, x375), x375)), x374)), x373, x374, pos(x375), x376))
(359) (minus_int(x370, x372)=x374∧pos(x371)=x1052∧plus_int(x1052, x370)=pos(x375) ⇒ EVAL(x369, x374, pos(x375), x372)≥COND_EVAL1(and(greatereq_int(x369, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x375, x375), x375)), x374)), x369, x374, pos(x375), x372))
(360) (minus_nat(x1054, x1053)=pos(x375)∧minus_int(neg(x1053), x372)=x374∧pos(x371)=pos(x1054) ⇒ EVAL(x369, x374, pos(x375), x372)≥COND_EVAL1(and(greatereq_int(x369, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x375, x375), x375)), x374)), x369, x374, pos(x375), x372))
(361) (minus_nat(x1055, x1056)=pos(x375)∧minus_int(pos(x1055), x372)=x374∧pos(x371)=neg(x1056) ⇒ EVAL(x369, x374, pos(x375), x372)≥COND_EVAL1(and(greatereq_int(x369, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x375, x375), x375)), x374)), x369, x374, pos(x375), x372))
(362) (pos(plus_nat(x1060, x1059))=pos(x375)∧minus_int(pos(x1059), x372)=x374∧pos(x371)=pos(x1060) ⇒ EVAL(x369, x374, pos(x375), x372)≥COND_EVAL1(and(greatereq_int(x369, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x375, x375), x375)), x374)), x369, x374, pos(x375), x372))
(363) (minus_nat(x1054, x1053)=pos(x375)∧neg(x1053)=x1061∧minus_int(x1061, x372)=x374 ⇒ EVAL(x369, x374, pos(x375), x372)≥COND_EVAL1(and(greatereq_int(x369, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x375, x375), x375)), x374)), x369, x374, pos(x375), x372))
(364) (pos(0)=pos(x375)∧neg(0)=x1061∧minus_int(x1061, x372)=x374 ⇒ EVAL(x369, x374, pos(x375), x372)≥COND_EVAL1(and(greatereq_int(x369, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x375, x375), x375)), x374)), x369, x374, pos(x375), x372))
(365) (pos(s(x1063))=pos(x375)∧neg(0)=x1061∧minus_int(x1061, x372)=x374 ⇒ EVAL(x369, x374, pos(x375), x372)≥COND_EVAL1(and(greatereq_int(x369, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x375, x375), x375)), x374)), x369, x374, pos(x375), x372))
(366) (minus_nat(x1065, x1064)=pos(x375)∧neg(s(x1064))=x1061∧minus_int(x1061, x372)=x374∧(∀x1066,x1067,x1068,x1069,x1070:minus_nat(x1065, x1064)=pos(x1066)∧neg(x1064)=x1067∧minus_int(x1067, x1068)=x1069 ⇒ EVAL(x1070, x1069, pos(x1066), x1068)≥COND_EVAL1(and(greatereq_int(x1070, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x1066, x1066), x1066)), x1069)), x1070, x1069, pos(x1066), x1068)) ⇒ EVAL(x369, x374, pos(x375), x372)≥COND_EVAL1(and(greatereq_int(x369, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x375, x375), x375)), x374)), x369, x374, pos(x375), x372))
(367) (EVAL(x369, x374, pos(0), x372)≥COND_EVAL1(and(greatereq_int(x369, pos(0)), greatereq_int(pos(mult_nat(mult_nat(0, 0), 0)), x374)), x369, x374, pos(0), x372))
(368) (EVAL(x369, x374, pos(s(x1063)), x372)≥COND_EVAL1(and(greatereq_int(x369, pos(0)), greatereq_int(pos(mult_nat(mult_nat(s(x1063), s(x1063)), s(x1063))), x374)), x369, x374, pos(s(x1063)), x372))
(369) (EVAL(x369, x374, pos(x375), x372)≥COND_EVAL1(and(greatereq_int(x369, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x375, x375), x375)), x374)), x369, x374, pos(x375), x372))
(370) (EVAL(x377, minus_int(x378, x380), plus_int(neg(x379), x378), x380)=EVAL(x381, x382, pos(x383), x384) ⇒ EVAL(x381, x382, pos(x383), x384)≥COND_EVAL1(and(greatereq_int(x381, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x383, x383), x383)), x382)), x381, x382, pos(x383), x384))
(371) (minus_int(x378, x380)=x382∧neg(x379)=x1072∧plus_int(x1072, x378)=pos(x383) ⇒ EVAL(x377, x382, pos(x383), x380)≥COND_EVAL1(and(greatereq_int(x377, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x383, x383), x383)), x382)), x377, x382, pos(x383), x380))
(372) (minus_nat(x1074, x1073)=pos(x383)∧minus_int(neg(x1073), x380)=x382∧neg(x379)=pos(x1074) ⇒ EVAL(x377, x382, pos(x383), x380)≥COND_EVAL1(and(greatereq_int(x377, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x383, x383), x383)), x382)), x377, x382, pos(x383), x380))
(373) (minus_nat(x1075, x1076)=pos(x383)∧minus_int(pos(x1075), x380)=x382∧neg(x379)=neg(x1076) ⇒ EVAL(x377, x382, pos(x383), x380)≥COND_EVAL1(and(greatereq_int(x377, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x383, x383), x383)), x382)), x377, x382, pos(x383), x380))
(374) (pos(plus_nat(x1080, x1079))=pos(x383)∧minus_int(pos(x1079), x380)=x382∧neg(x379)=pos(x1080) ⇒ EVAL(x377, x382, pos(x383), x380)≥COND_EVAL1(and(greatereq_int(x377, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x383, x383), x383)), x382)), x377, x382, pos(x383), x380))
(375) (minus_nat(x1075, x1076)=pos(x383)∧pos(x1075)=x1081∧minus_int(x1081, x380)=x382 ⇒ EVAL(x377, x382, pos(x383), x380)≥COND_EVAL1(and(greatereq_int(x377, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x383, x383), x383)), x382)), x377, x382, pos(x383), x380))
(376) (pos(0)=pos(x383)∧pos(0)=x1081∧minus_int(x1081, x380)=x382 ⇒ EVAL(x377, x382, pos(x383), x380)≥COND_EVAL1(and(greatereq_int(x377, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x383, x383), x383)), x382)), x377, x382, pos(x383), x380))
(377) (pos(s(x1083))=pos(x383)∧pos(s(x1083))=x1081∧minus_int(x1081, x380)=x382 ⇒ EVAL(x377, x382, pos(x383), x380)≥COND_EVAL1(and(greatereq_int(x377, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x383, x383), x383)), x382)), x377, x382, pos(x383), x380))
(378) (minus_nat(x1085, x1084)=pos(x383)∧pos(s(x1085))=x1081∧minus_int(x1081, x380)=x382∧(∀x1086,x1087,x1088,x1089,x1090:minus_nat(x1085, x1084)=pos(x1086)∧pos(x1085)=x1087∧minus_int(x1087, x1088)=x1089 ⇒ EVAL(x1090, x1089, pos(x1086), x1088)≥COND_EVAL1(and(greatereq_int(x1090, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x1086, x1086), x1086)), x1089)), x1090, x1089, pos(x1086), x1088)) ⇒ EVAL(x377, x382, pos(x383), x380)≥COND_EVAL1(and(greatereq_int(x377, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x383, x383), x383)), x382)), x377, x382, pos(x383), x380))
(379) (EVAL(x377, x382, pos(0), x380)≥COND_EVAL1(and(greatereq_int(x377, pos(0)), greatereq_int(pos(mult_nat(mult_nat(0, 0), 0)), x382)), x377, x382, pos(0), x380))
(380) (EVAL(x377, x382, pos(s(x1083)), x380)≥COND_EVAL1(and(greatereq_int(x377, pos(0)), greatereq_int(pos(mult_nat(mult_nat(s(x1083), s(x1083)), s(x1083))), x382)), x377, x382, pos(s(x1083)), x380))
(381) (EVAL(x377, x382, pos(x383), x380)≥COND_EVAL1(and(greatereq_int(x377, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x383, x383), x383)), x382)), x377, x382, pos(x383), x380))
(382) (EVAL(neg(0), minus_int(x385, x387), plus_int(x386, x385), x387)=EVAL(x388, x389, pos(x390), x391) ⇒ EVAL(x388, x389, pos(x390), x391)≥COND_EVAL1(and(greatereq_int(x388, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x390, x390), x390)), x389)), x388, x389, pos(x390), x391))
(383) (minus_int(x385, x387)=x389∧plus_int(x386, x385)=pos(x390) ⇒ EVAL(neg(0), x389, pos(x390), x387)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x390, x390), x390)), x389)), neg(0), x389, pos(x390), x387))
(384) (minus_nat(x1092, x1091)=pos(x390)∧minus_int(neg(x1091), x387)=x389 ⇒ EVAL(neg(0), x389, pos(x390), x387)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x390, x390), x390)), x389)), neg(0), x389, pos(x390), x387))
(385) (minus_nat(x1093, x1094)=pos(x390)∧minus_int(pos(x1093), x387)=x389 ⇒ EVAL(neg(0), x389, pos(x390), x387)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x390, x390), x390)), x389)), neg(0), x389, pos(x390), x387))
(386) (pos(plus_nat(x1098, x1097))=pos(x390)∧minus_int(pos(x1097), x387)=x389 ⇒ EVAL(neg(0), x389, pos(x390), x387)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x390, x390), x390)), x389)), neg(0), x389, pos(x390), x387))
(387) (minus_nat(x1092, x1091)=pos(x390)∧neg(x1091)=x1099∧minus_int(x1099, x387)=x389 ⇒ EVAL(neg(0), x389, pos(x390), x387)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x390, x390), x390)), x389)), neg(0), x389, pos(x390), x387))
(388) (minus_nat(x1093, x1094)=pos(x390)∧pos(x1093)=x1108∧minus_int(x1108, x387)=x389 ⇒ EVAL(neg(0), x389, pos(x390), x387)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x390, x390), x390)), x389)), neg(0), x389, pos(x390), x387))
(389) (pos(0)=pos(x390)∧neg(0)=x1099∧minus_int(x1099, x387)=x389 ⇒ EVAL(neg(0), x389, pos(x390), x387)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x390, x390), x390)), x389)), neg(0), x389, pos(x390), x387))
(390) (pos(s(x1101))=pos(x390)∧neg(0)=x1099∧minus_int(x1099, x387)=x389 ⇒ EVAL(neg(0), x389, pos(x390), x387)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x390, x390), x390)), x389)), neg(0), x389, pos(x390), x387))
(391) (minus_nat(x1103, x1102)=pos(x390)∧neg(s(x1102))=x1099∧minus_int(x1099, x387)=x389∧(∀x1104,x1105,x1106,x1107:minus_nat(x1103, x1102)=pos(x1104)∧neg(x1102)=x1105∧minus_int(x1105, x1106)=x1107 ⇒ EVAL(neg(0), x1107, pos(x1104), x1106)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x1104, x1104), x1104)), x1107)), neg(0), x1107, pos(x1104), x1106)) ⇒ EVAL(neg(0), x389, pos(x390), x387)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x390, x390), x390)), x389)), neg(0), x389, pos(x390), x387))
(392) (EVAL(neg(0), x389, pos(0), x387)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(pos(mult_nat(mult_nat(0, 0), 0)), x389)), neg(0), x389, pos(0), x387))
(393) (EVAL(neg(0), x389, pos(s(x1101)), x387)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(pos(mult_nat(mult_nat(s(x1101), s(x1101)), s(x1101))), x389)), neg(0), x389, pos(s(x1101)), x387))
(394) (EVAL(neg(0), x389, pos(x390), x387)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x390, x390), x390)), x389)), neg(0), x389, pos(x390), x387))
(395) (pos(0)=pos(x390)∧pos(0)=x1108∧minus_int(x1108, x387)=x389 ⇒ EVAL(neg(0), x389, pos(x390), x387)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x390, x390), x390)), x389)), neg(0), x389, pos(x390), x387))
(396) (pos(s(x1110))=pos(x390)∧pos(s(x1110))=x1108∧minus_int(x1108, x387)=x389 ⇒ EVAL(neg(0), x389, pos(x390), x387)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x390, x390), x390)), x389)), neg(0), x389, pos(x390), x387))
(397) (minus_nat(x1112, x1111)=pos(x390)∧pos(s(x1112))=x1108∧minus_int(x1108, x387)=x389∧(∀x1113,x1114,x1115,x1116:minus_nat(x1112, x1111)=pos(x1113)∧pos(x1112)=x1114∧minus_int(x1114, x1115)=x1116 ⇒ EVAL(neg(0), x1116, pos(x1113), x1115)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x1113, x1113), x1113)), x1116)), neg(0), x1116, pos(x1113), x1115)) ⇒ EVAL(neg(0), x389, pos(x390), x387)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x390, x390), x390)), x389)), neg(0), x389, pos(x390), x387))
(398) (EVAL(neg(0), x389, pos(0), x387)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(pos(mult_nat(mult_nat(0, 0), 0)), x389)), neg(0), x389, pos(0), x387))
(399) (EVAL(neg(0), x389, pos(s(x1110)), x387)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(pos(mult_nat(mult_nat(s(x1110), s(x1110)), s(x1110))), x389)), neg(0), x389, pos(s(x1110)), x387))
(400) (EVAL(neg(0), x389, pos(x390), x387)≥COND_EVAL1(and(greatereq_int(neg(0), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x390, x390), x390)), x389)), neg(0), x389, pos(x390), x387))
(401) (EVAL(pos(x396), minus_int(x397, x399), plus_int(x398, x397), x399)=EVAL(x400, x401, pos(x402), x403) ⇒ EVAL(x400, x401, pos(x402), x403)≥COND_EVAL1(and(greatereq_int(x400, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x402, x402), x402)), x401)), x400, x401, pos(x402), x403))
(402) (minus_int(x397, x399)=x401∧plus_int(x398, x397)=pos(x402) ⇒ EVAL(pos(x396), x401, pos(x402), x399)≥COND_EVAL1(and(greatereq_int(pos(x396), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x402, x402), x402)), x401)), pos(x396), x401, pos(x402), x399))
(403) (minus_nat(x1119, x1118)=pos(x402)∧minus_int(neg(x1118), x399)=x401 ⇒ EVAL(pos(x396), x401, pos(x402), x399)≥COND_EVAL1(and(greatereq_int(pos(x396), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x402, x402), x402)), x401)), pos(x396), x401, pos(x402), x399))
(404) (minus_nat(x1120, x1121)=pos(x402)∧minus_int(pos(x1120), x399)=x401 ⇒ EVAL(pos(x396), x401, pos(x402), x399)≥COND_EVAL1(and(greatereq_int(pos(x396), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x402, x402), x402)), x401)), pos(x396), x401, pos(x402), x399))
(405) (pos(plus_nat(x1125, x1124))=pos(x402)∧minus_int(pos(x1124), x399)=x401 ⇒ EVAL(pos(x396), x401, pos(x402), x399)≥COND_EVAL1(and(greatereq_int(pos(x396), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x402, x402), x402)), x401)), pos(x396), x401, pos(x402), x399))
(406) (minus_nat(x1119, x1118)=pos(x402)∧neg(x1118)=x1126∧minus_int(x1126, x399)=x401 ⇒ EVAL(pos(x396), x401, pos(x402), x399)≥COND_EVAL1(and(greatereq_int(pos(x396), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x402, x402), x402)), x401)), pos(x396), x401, pos(x402), x399))
(407) (minus_nat(x1120, x1121)=pos(x402)∧pos(x1120)=x1136∧minus_int(x1136, x399)=x401 ⇒ EVAL(pos(x396), x401, pos(x402), x399)≥COND_EVAL1(and(greatereq_int(pos(x396), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x402, x402), x402)), x401)), pos(x396), x401, pos(x402), x399))
(408) (pos(0)=pos(x402)∧neg(0)=x1126∧minus_int(x1126, x399)=x401 ⇒ EVAL(pos(x396), x401, pos(x402), x399)≥COND_EVAL1(and(greatereq_int(pos(x396), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x402, x402), x402)), x401)), pos(x396), x401, pos(x402), x399))
(409) (pos(s(x1128))=pos(x402)∧neg(0)=x1126∧minus_int(x1126, x399)=x401 ⇒ EVAL(pos(x396), x401, pos(x402), x399)≥COND_EVAL1(and(greatereq_int(pos(x396), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x402, x402), x402)), x401)), pos(x396), x401, pos(x402), x399))
(410) (minus_nat(x1130, x1129)=pos(x402)∧neg(s(x1129))=x1126∧minus_int(x1126, x399)=x401∧(∀x1131,x1132,x1133,x1134,x1135:minus_nat(x1130, x1129)=pos(x1131)∧neg(x1129)=x1132∧minus_int(x1132, x1133)=x1134 ⇒ EVAL(pos(x1135), x1134, pos(x1131), x1133)≥COND_EVAL1(and(greatereq_int(pos(x1135), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x1131, x1131), x1131)), x1134)), pos(x1135), x1134, pos(x1131), x1133)) ⇒ EVAL(pos(x396), x401, pos(x402), x399)≥COND_EVAL1(and(greatereq_int(pos(x396), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x402, x402), x402)), x401)), pos(x396), x401, pos(x402), x399))
(411) (EVAL(pos(x396), x401, pos(0), x399)≥COND_EVAL1(and(greatereq_int(pos(x396), pos(0)), greatereq_int(pos(mult_nat(mult_nat(0, 0), 0)), x401)), pos(x396), x401, pos(0), x399))
(412) (EVAL(pos(x396), x401, pos(s(x1128)), x399)≥COND_EVAL1(and(greatereq_int(pos(x396), pos(0)), greatereq_int(pos(mult_nat(mult_nat(s(x1128), s(x1128)), s(x1128))), x401)), pos(x396), x401, pos(s(x1128)), x399))
(413) (EVAL(pos(x396), x401, pos(x402), x399)≥COND_EVAL1(and(greatereq_int(pos(x396), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x402, x402), x402)), x401)), pos(x396), x401, pos(x402), x399))
(414) (pos(0)=pos(x402)∧pos(0)=x1136∧minus_int(x1136, x399)=x401 ⇒ EVAL(pos(x396), x401, pos(x402), x399)≥COND_EVAL1(and(greatereq_int(pos(x396), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x402, x402), x402)), x401)), pos(x396), x401, pos(x402), x399))
(415) (pos(s(x1138))=pos(x402)∧pos(s(x1138))=x1136∧minus_int(x1136, x399)=x401 ⇒ EVAL(pos(x396), x401, pos(x402), x399)≥COND_EVAL1(and(greatereq_int(pos(x396), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x402, x402), x402)), x401)), pos(x396), x401, pos(x402), x399))
(416) (minus_nat(x1140, x1139)=pos(x402)∧pos(s(x1140))=x1136∧minus_int(x1136, x399)=x401∧(∀x1141,x1142,x1143,x1144,x1145:minus_nat(x1140, x1139)=pos(x1141)∧pos(x1140)=x1142∧minus_int(x1142, x1143)=x1144 ⇒ EVAL(pos(x1145), x1144, pos(x1141), x1143)≥COND_EVAL1(and(greatereq_int(pos(x1145), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x1141, x1141), x1141)), x1144)), pos(x1145), x1144, pos(x1141), x1143)) ⇒ EVAL(pos(x396), x401, pos(x402), x399)≥COND_EVAL1(and(greatereq_int(pos(x396), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x402, x402), x402)), x401)), pos(x396), x401, pos(x402), x399))
(417) (EVAL(pos(x396), x401, pos(0), x399)≥COND_EVAL1(and(greatereq_int(pos(x396), pos(0)), greatereq_int(pos(mult_nat(mult_nat(0, 0), 0)), x401)), pos(x396), x401, pos(0), x399))
(418) (EVAL(pos(x396), x401, pos(s(x1138)), x399)≥COND_EVAL1(and(greatereq_int(pos(x396), pos(0)), greatereq_int(pos(mult_nat(mult_nat(s(x1138), s(x1138)), s(x1138))), x401)), pos(x396), x401, pos(s(x1138)), x399))
(419) (EVAL(pos(x396), x401, pos(x402), x399)≥COND_EVAL1(and(greatereq_int(pos(x396), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x402, x402), x402)), x401)), pos(x396), x401, pos(x402), x399))
(420) (EVAL(neg(s(x408)), minus_int(x409, x411), plus_int(x410, x409), x411)=EVAL(x412, x413, pos(x414), x415) ⇒ EVAL(x412, x413, pos(x414), x415)≥COND_EVAL1(and(greatereq_int(x412, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x414, x414), x414)), x413)), x412, x413, pos(x414), x415))
(421) (minus_int(x409, x411)=x413∧plus_int(x410, x409)=pos(x414) ⇒ EVAL(neg(s(x408)), x413, pos(x414), x411)≥COND_EVAL1(and(greatereq_int(neg(s(x408)), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x414, x414), x414)), x413)), neg(s(x408)), x413, pos(x414), x411))
(422) (minus_nat(x1148, x1147)=pos(x414)∧minus_int(neg(x1147), x411)=x413 ⇒ EVAL(neg(s(x408)), x413, pos(x414), x411)≥COND_EVAL1(and(greatereq_int(neg(s(x408)), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x414, x414), x414)), x413)), neg(s(x408)), x413, pos(x414), x411))
(423) (minus_nat(x1149, x1150)=pos(x414)∧minus_int(pos(x1149), x411)=x413 ⇒ EVAL(neg(s(x408)), x413, pos(x414), x411)≥COND_EVAL1(and(greatereq_int(neg(s(x408)), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x414, x414), x414)), x413)), neg(s(x408)), x413, pos(x414), x411))
(424) (pos(plus_nat(x1154, x1153))=pos(x414)∧minus_int(pos(x1153), x411)=x413 ⇒ EVAL(neg(s(x408)), x413, pos(x414), x411)≥COND_EVAL1(and(greatereq_int(neg(s(x408)), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x414, x414), x414)), x413)), neg(s(x408)), x413, pos(x414), x411))
(425) (minus_nat(x1148, x1147)=pos(x414)∧neg(x1147)=x1155∧minus_int(x1155, x411)=x413 ⇒ EVAL(neg(s(x408)), x413, pos(x414), x411)≥COND_EVAL1(and(greatereq_int(neg(s(x408)), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x414, x414), x414)), x413)), neg(s(x408)), x413, pos(x414), x411))
(426) (minus_nat(x1149, x1150)=pos(x414)∧pos(x1149)=x1165∧minus_int(x1165, x411)=x413 ⇒ EVAL(neg(s(x408)), x413, pos(x414), x411)≥COND_EVAL1(and(greatereq_int(neg(s(x408)), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x414, x414), x414)), x413)), neg(s(x408)), x413, pos(x414), x411))
(427) (pos(0)=pos(x414)∧neg(0)=x1155∧minus_int(x1155, x411)=x413 ⇒ EVAL(neg(s(x408)), x413, pos(x414), x411)≥COND_EVAL1(and(greatereq_int(neg(s(x408)), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x414, x414), x414)), x413)), neg(s(x408)), x413, pos(x414), x411))
(428) (pos(s(x1157))=pos(x414)∧neg(0)=x1155∧minus_int(x1155, x411)=x413 ⇒ EVAL(neg(s(x408)), x413, pos(x414), x411)≥COND_EVAL1(and(greatereq_int(neg(s(x408)), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x414, x414), x414)), x413)), neg(s(x408)), x413, pos(x414), x411))
(429) (minus_nat(x1159, x1158)=pos(x414)∧neg(s(x1158))=x1155∧minus_int(x1155, x411)=x413∧(∀x1160,x1161,x1162,x1163,x1164:minus_nat(x1159, x1158)=pos(x1160)∧neg(x1158)=x1161∧minus_int(x1161, x1162)=x1163 ⇒ EVAL(neg(s(x1164)), x1163, pos(x1160), x1162)≥COND_EVAL1(and(greatereq_int(neg(s(x1164)), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x1160, x1160), x1160)), x1163)), neg(s(x1164)), x1163, pos(x1160), x1162)) ⇒ EVAL(neg(s(x408)), x413, pos(x414), x411)≥COND_EVAL1(and(greatereq_int(neg(s(x408)), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x414, x414), x414)), x413)), neg(s(x408)), x413, pos(x414), x411))
(430) (EVAL(neg(s(x408)), x413, pos(0), x411)≥COND_EVAL1(and(greatereq_int(neg(s(x408)), pos(0)), greatereq_int(pos(mult_nat(mult_nat(0, 0), 0)), x413)), neg(s(x408)), x413, pos(0), x411))
(431) (EVAL(neg(s(x408)), x413, pos(s(x1157)), x411)≥COND_EVAL1(and(greatereq_int(neg(s(x408)), pos(0)), greatereq_int(pos(mult_nat(mult_nat(s(x1157), s(x1157)), s(x1157))), x413)), neg(s(x408)), x413, pos(s(x1157)), x411))
(432) (EVAL(neg(s(x408)), x413, pos(x414), x411)≥COND_EVAL1(and(greatereq_int(neg(s(x408)), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x414, x414), x414)), x413)), neg(s(x408)), x413, pos(x414), x411))
(433) (pos(0)=pos(x414)∧pos(0)=x1165∧minus_int(x1165, x411)=x413 ⇒ EVAL(neg(s(x408)), x413, pos(x414), x411)≥COND_EVAL1(and(greatereq_int(neg(s(x408)), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x414, x414), x414)), x413)), neg(s(x408)), x413, pos(x414), x411))
(434) (pos(s(x1167))=pos(x414)∧pos(s(x1167))=x1165∧minus_int(x1165, x411)=x413 ⇒ EVAL(neg(s(x408)), x413, pos(x414), x411)≥COND_EVAL1(and(greatereq_int(neg(s(x408)), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x414, x414), x414)), x413)), neg(s(x408)), x413, pos(x414), x411))
(435) (minus_nat(x1169, x1168)=pos(x414)∧pos(s(x1169))=x1165∧minus_int(x1165, x411)=x413∧(∀x1170,x1171,x1172,x1173,x1174:minus_nat(x1169, x1168)=pos(x1170)∧pos(x1169)=x1171∧minus_int(x1171, x1172)=x1173 ⇒ EVAL(neg(s(x1174)), x1173, pos(x1170), x1172)≥COND_EVAL1(and(greatereq_int(neg(s(x1174)), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x1170, x1170), x1170)), x1173)), neg(s(x1174)), x1173, pos(x1170), x1172)) ⇒ EVAL(neg(s(x408)), x413, pos(x414), x411)≥COND_EVAL1(and(greatereq_int(neg(s(x408)), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x414, x414), x414)), x413)), neg(s(x408)), x413, pos(x414), x411))
(436) (EVAL(neg(s(x408)), x413, pos(0), x411)≥COND_EVAL1(and(greatereq_int(neg(s(x408)), pos(0)), greatereq_int(pos(mult_nat(mult_nat(0, 0), 0)), x413)), neg(s(x408)), x413, pos(0), x411))
(437) (EVAL(neg(s(x408)), x413, pos(s(x1167)), x411)≥COND_EVAL1(and(greatereq_int(neg(s(x408)), pos(0)), greatereq_int(pos(mult_nat(mult_nat(s(x1167), s(x1167)), s(x1167))), x413)), neg(s(x408)), x413, pos(s(x1167)), x411))
(438) (EVAL(neg(s(x408)), x413, pos(x414), x411)≥COND_EVAL1(and(greatereq_int(neg(s(x408)), pos(0)), greatereq_int(pos(mult_nat(mult_nat(x414, x414), x414)), x413)), neg(s(x408)), x413, pos(x414), x411))
POL(0) = 1
POL(COND_EVAL1(x1, x2, x3, x4, x5)) = -1 - x1 - x2 - x3 - x4 - x5
POL(EVAL(x1, x2, x3, x4)) = -1 + x1 - x2 - x3 - x4
POL(and(x1, x2)) = 0
POL(c) = -1
POL(false) = 1
POL(greatereq_int(x1, x2)) = 0
POL(minus_int(x1, x2)) = 0
POL(minus_nat(x1, x2)) = 0
POL(mult_int(x1, x2)) = 0
POL(mult_nat(x1, x2)) = 0
POL(neg(x1)) = 0
POL(plus_int(x1, x2)) = x1
POL(plus_nat(x1, x2)) = 1 + x1 + x2
POL(pos(x1)) = 0
POL(s(x1)) = 0
POL(true) = 0
The following pairs are in Pbound:
COND_EVAL1(true, neg(s(z0)), z1, z2, x_removed) → EVAL(neg(s(z0)), minus_int(z1, x_removed), plus_int(z2, z1), x_removed)
The following rules are usable:
COND_EVAL1(true, neg(s(z0)), z1, z2, x_removed) → EVAL(neg(s(z0)), minus_int(z1, x_removed), plus_int(z2, z1), x_removed)
pos(0) → minus_nat(0, 0)
pos(plus_nat(x, y)) → plus_int(pos(x), pos(y))
neg(plus_nat(x, y)) → plus_int(neg(x), neg(y))
minus_nat(y, x) → plus_int(neg(x), pos(y))
minus_nat(x, y) → plus_int(pos(x), neg(y))
neg(plus_nat(x, y)) → minus_int(neg(x), pos(y))
minus_nat(x, y) → minus_int(pos(x), pos(y))
true → and(true, true)
false → and(true, false)
false → and(false, true)
false → and(false, false)
minus_nat(x, y) → minus_nat(s(x), s(y))
neg(s(y)) → minus_nat(0, s(y))
pos(s(x)) → minus_nat(s(x), 0)
↳ ITRS
↳ ITRStoIDPProof
↳ IDP
↳ UsableRulesProof
↳ IDP
↳ IDPNonInfProof
↳ IDP
↳ IDependencyGraphProof
↳ IDP
↳ IDPtoQDPProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ RemovalProof
↳ QDP
↳ NonInfProof
↳ QDP
EVAL(neg(0), y1, y2, x_removed) → COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), neg(0), y1, y2, x_removed)
COND_EVAL1(true, z0, z1, pos(z2), x_removed) → EVAL(z0, minus_int(z1, x_removed), plus_int(pos(z2), z1), x_removed)
COND_EVAL1(true, z0, z1, neg(z2), x_removed) → EVAL(z0, minus_int(z1, x_removed), plus_int(neg(z2), z1), x_removed)
COND_EVAL1(true, neg(0), z0, z1, x_removed) → EVAL(neg(0), minus_int(z0, x_removed), plus_int(z1, z0), x_removed)
EVAL(pos(x0), y1, y2, x_removed) → COND_EVAL1(and(true, greatereq_int(mult_int(mult_int(y2, y2), y2), y1)), pos(x0), y1, y2, x_removed)
COND_EVAL1(true, pos(z0), z1, z2, x_removed) → EVAL(pos(z0), minus_int(z1, x_removed), plus_int(z2, z1), x_removed)
EVAL(y0, y1, neg(x0), x_removed) → COND_EVAL1(and(greatereq_int(y0, pos(0)), greatereq_int(neg(mult_nat(mult_nat(x0, x0), x0)), y1)), y0, y1, neg(x0), x_removed)
EVAL(y0, y1, pos(x0), x_removed) → COND_EVAL1(and(greatereq_int(y0, pos(0)), greatereq_int(pos(mult_nat(mult_nat(x0, x0), x0)), y1)), y0, y1, pos(x0), x_removed)
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_int(pos(x), pos(y)) → minus_nat(x, y)
minus_int(neg(x), pos(y)) → neg(plus_nat(x, y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_int(pos(x0), pos(x1))
minus_int(neg(x0), neg(x1))
minus_int(neg(x0), pos(x1))
minus_int(pos(x0), neg(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))